defectDist_symm

formal source

 316  exact J_at_one
 317
 318/-- **PROVED: Defect distance is symmetric.** -/
 319theorem defectDist_symm (x y : ℝ) (hx : 0 < x) (hy : 0 < y) :
 320    defectDist x y = defectDist y x := by
 321  unfold defectDist
 322  have h : x / y > 0 := div_pos hx hy
 323  rw [J_reciprocal (x / y) h]
 324  congr 1
 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