theorem
proved
eulerScalarProxy_pos
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Unification.UnifiedRH on GitHub at line 177.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
-
reciprocal -
of -
of -
defect -
reciprocal -
of -
of -
of -
DefectSensor -
eulerScalarGap -
eulerScalarGap_pos -
eulerScalarProxy
used by
formal source
174 1 / (1 + eulerScalarGap sensor / (N + 1 : ℝ))
175
176/-- The concrete Euler scalar proxy stays positive at every refinement depth. -/
177theorem eulerScalarProxy_pos (sensor : DefectSensor) (N : ℕ) :
178 0 < eulerScalarProxy sensor N := by
179 unfold eulerScalarProxy
180 apply one_div_pos.mpr
181 have hgap_nonneg : 0 ≤ eulerScalarGap sensor := le_of_lt (eulerScalarGap_pos sensor)
182 have hfrac_nonneg : 0 ≤ eulerScalarGap sensor / (N + 1 : ℝ) := by
183 exact div_nonneg hgap_nonneg (by positivity)
184 linarith
185
186/-- Closed form of the T1 defect on the reciprocal-affine Euler scalar proxy. -/
187private theorem defect_one_div_one_add (t : ℝ) (ht : 0 ≤ t) :
188 IndisputableMonolith.Foundation.LawOfExistence.defect (1 / (1 + t)) =
189 t ^ 2 / (2 * (1 + t)) := by
190 unfold IndisputableMonolith.Foundation.LawOfExistence.defect
191 IndisputableMonolith.Foundation.LawOfExistence.J
192 have hden : (1 + t : ℝ) ≠ 0 := by linarith
193 field_simp [hden]
194 ring
195
196/-- The Euler scalar proxy has uniformly bounded T1 defect. -/
197theorem eulerScalarProxy_defect_bounded (sensor : DefectSensor) :
198 ∃ K : ℝ, ∀ N : ℕ,
199 IndisputableMonolith.Foundation.LawOfExistence.defect
200 (eulerScalarProxy sensor N) ≤ K := by
201 refine ⟨(eulerScalarGap sensor) ^ 2 / 2, ?_⟩
202 intro N
203 let t : ℝ := eulerScalarGap sensor / (N + 1 : ℝ)
204 have ht_nonneg : 0 ≤ t := by
205 unfold t
206 exact div_nonneg (le_of_lt (eulerScalarGap_pos sensor)) (by positivity)
207 rw [eulerScalarProxy, defect_one_div_one_add t ht_nonneg]