eulerScalarProxy_defect_bounded

formal source

 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]
 208  have hden :
 209      (2 : ℝ) ≤ 2 * (1 + t) := by
 210    nlinarith [ht_nonneg]
 211  have hstep1 :
 212      t ^ 2 / (2 * (1 + t)) ≤ t ^ 2 / 2 := by
 213    exact div_le_div_of_nonneg_left (sq_nonneg t) (by positivity) hden
 214  have ht_le_gap :
 215      t ≤ eulerScalarGap sensor := by
 216    unfold t
 217    have hgap_nonneg : 0 ≤ eulerScalarGap sensor := le_of_lt (eulerScalarGap_pos sensor)
 218    have hone_le_nat : (1 : ℕ) ≤ N + 1 := by
 219      exact Nat.succ_le_succ (Nat.zero_le N)
 220    have hone_le : (1 : ℝ) ≤ (N + 1 : ℝ) := by
 221      exact_mod_cast hone_le_nat
 222    exact div_le_self hgap_nonneg hone_le
 223  have hsq :
 224      t ^ 2 ≤ (eulerScalarGap sensor) ^ 2 := by
 225    nlinarith [ht_nonneg, le_of_lt (eulerScalarGap_pos sensor), ht_le_gap]
 226  have hstep2 :
 227      t ^ 2 / 2 ≤ (eulerScalarGap sensor) ^ 2 / 2 := by