eulerSampledBudgetedCarrier

formal source

 956The key difference from `eulerBudgetedCarrier` is that the zero-winding
 957property is derived from the carrier's holomorphy and nonvanishing
 958(via `eulerZeroWindingCert`), not assumed. -/
 959noncomputable def eulerSampledBudgetedCarrier (σ₀ : ℝ) (hσ : 1/2 < σ₀) :
 960    BudgetedCarrier :=
 961  SampledTrace.sampledBudgetedCarrier
 962    (EulerCarrierComplex.eulerZeroWindingCert σ₀ hσ)
 963    (carrierDerivBound σ₀)
 964    (carrierDerivBound_pos hσ)
 965    (σ₀ - 1/2)
 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]