defect_one_div_one_add

formal source

 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]
 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)