defectDist_self

formal source

 310noncomputable def defectDist (x y : ℝ) : ℝ := J (x / y)
 311
 312/-- **PROVED: Defect distance is zero at identity.** -/
 313theorem defectDist_self (x : ℝ) (hx : 0 < x) : defectDist x x = 0 := by
 314  unfold defectDist
 315  rw [div_self (ne_of_gt hx)]
 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