`eulerSampledBudgetedCarrier_scale_zero`

proved

show as: view math explainer →

module: IndisputableMonolith.NumberTheory.EulerInstantiation
domain: NumberTheory
line: 969 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.NumberTheory.EulerInstantiation on GitHub at line 969.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

 966    (by linarith)
 967
 968/-- The sampled Euler carrier has budget scale 0. -/
 969theorem eulerSampledBudgetedCarrier_scale_zero (σ₀ : ℝ) (hσ : 1/2 < σ₀) :
 970    carrierBudgetScale (eulerSampledBudgetedCarrier σ₀ hσ) = 0 := by
 971  simp [eulerSampledBudgetedCarrier, SampledTrace.sampledBudgetedCarrier, carrierBudgetScale]
 972
 973/-- Package the sampled Euler carrier as a `CostCoveringPackage`. -/
 974noncomputable def eulerSampledPackage (σ₀ : ℝ) (hσ : 1/2 < σ₀) :
 975    CostCoveringPackage where
 976  carrier := eulerSampledBudgetedCarrier σ₀ hσ
 977
 978/-- The sampled package's floor coverage is equivalent to charge = 0. -/
 979theorem eulerSampledFloorCovered_iff_charge_zero (σ₀ : ℝ) (hσ : 1/2 < σ₀)
 980    (sensor : DefectSensor) :
 981    DefectTopologicalFloorCovered (eulerSampledPackage σ₀ hσ) sensor ↔
 982      sensor.charge = 0 := by
 983  constructor
 984  · intro hcover
 985    by_contra hm
 986    exact not_DefectTopologicalFloorCovered (eulerSampledPackage σ₀ hσ) sensor hm hcover
 987  · intro hzero
 988    intro N
 989    rw [hzero, annularTopologicalFloor_zero]
 990    exact carrierBudgetScale_nonneg _
 991
 992end NumberTheory
 993end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.