defectDist_nonneg

formal source

 325  field_simp
 326
 327/-- **PROVED: Defect distance is non-negative.** -/
 328theorem defectDist_nonneg (x y : ℝ) (hx : 0 < x) (hy : 0 < y) :
 329    0 ≤ defectDist x y :=
 330  J_nonneg (x / y) (div_pos hx hy)
 331
 332/-! ## §5a. Quasi-Triangle Bounds for the Defect Distance -/
 333
 334/-- On the symmetric interval `[1 / M, M]`, the canonical cost is bounded by
 335    its endpoint value `J(M)`. -/
 336theorem J_le_J_of_inv_le_le {r M : ℝ} (hM : 1 ≤ M) (hr : 0 < r)
 337    (hr_lower : 1 / M ≤ r) (hr_upper : r ≤ M) :
 338    J r ≤ J M := by
 339  have hMpos : 0 < M := lt_of_lt_of_le (by norm_num : (0 : ℝ) < 1) hM
 340  have hfactor :
 341      M + M⁻¹ - (r + r⁻¹) = ((M - r) * (M * r - 1)) / (M * r) := by
 342    field_simp [hMpos.ne', hr.ne']
 343    ring
 344  have hMr_ge_one : 1 ≤ M * r := by
 345    have hmul := mul_le_mul_of_nonneg_left hr_lower (le_of_lt hMpos)
 346    simpa [one_div, hMpos.ne'] using hmul
 347  have hnum_nonneg : 0 ≤ (M - r) * (M * r - 1) := by
 348    have h1 : 0 ≤ M - r := sub_nonneg.mpr hr_upper
 349    have h2 : 0 ≤ M * r - 1 := by linarith
 350    exact mul_nonneg h1 h2
 351  have hden_pos : 0 < M * r := mul_pos hMpos hr
 352  have hsum_le : r + r⁻¹ ≤ M + M⁻¹ := by
 353    have hdiff_nonneg : 0 ≤ M + M⁻¹ - (r + r⁻¹) := by
 354      rw [hfactor]
 355      exact div_nonneg hnum_nonneg (le_of_lt hden_pos)
 356    linarith
 357  unfold J Jcost
 358  linarith