J_symmetric

formal source

 135/-! ## Key Properties of J -/
 136
 137/-- J is symmetric: J(x) = J(1/x) for positive x. -/
 138theorem J_symmetric {x : ℝ} (hx : 0 < x) : J x = J x⁻¹ := by
 139  have hx0 : x ≠ 0 := hx.ne'
 140  simp only [J]
 141  field_simp
 142  ring
 143
 144/-- J is non-negative for positive x (AM-GM inequality). -/
 145theorem J_nonneg {x : ℝ} (hx : 0 < x) : 0 ≤ J x := by
 146  simp only [J]
 147  have h : 0 ≤ (x - 1)^2 / x := by positivity
 148  calc (x + x⁻¹) / 2 - 1 = ((x - 1)^2 / x) / 2 := by field_simp; ring
 149    _ ≥ 0 := by positivity
 150
 151/-- J equals zero exactly at x = 1. -/
 152theorem J_eq_zero_iff {x : ℝ} (hx : 0 < x) : J x = 0 ↔ x = 1 := by
 153  constructor
 154  · intro hJ
 155    simp only [J] at hJ
 156    -- (x + 1/x)/2 - 1 = 0  ⟹  x + 1/x = 2  ⟹  x² - 2x + 1 = 0  ⟹  x = 1
 157    have h1 : x + x⁻¹ = 2 := by linarith
 158    have hx0 : x ≠ 0 := hx.ne'
 159    have h2 : x^2 + 1 = 2 * x := by
 160      field_simp at h1
 161      linarith
 162    have h3 : (x - 1)^2 = 0 := by ring_nf; linarith
 163    have h4 : x - 1 = 0 := by nlinarith [sq_nonneg (x - 1)]
 164    linarith
 165  · intro hx1
 166    simp [J, hx1]
 167
 168/-! ## The Economic Inevitability: J(0) → ∞ -/