geometricMean

formal source

 106/-! ## §3. Geometric-mean optimality -/
 107
 108/-- **F1.3.2**: The geometric mean of a list of positive reals -/
 109noncomputable def geometricMean (ns : List ℝ) : ℝ :=
 110  Real.exp ((ns.map Real.log).sum / ns.length)
 111
 112/-- The geometric mean of positive reals is positive -/
 113theorem geometricMean_pos {ns : List ℝ} (hns : ∀ n ∈ ns, 0 < n) (hne : ns ≠ []) :
 114    0 < geometricMean ns := by
 115  unfold geometricMean
 116  exact Real.exp_pos _
 117
 118/-- **F1.3.2 (two-element case)**: For two positive reals, the geometric mean
 119    minimizes the total J-cost. We prove the key fact: at the geometric mean,
 120    the J-cost is symmetric in the two neighbors. -/
 121theorem totalJcost_at_geomean_symmetric {n₁ n₂ : ℝ} (hn₁ : 0 < n₁) (hn₂ : 0 < n₂) :
 122    let gm := Real.sqrt (n₁ * n₂)
 123    Jcost (gm / n₁) = Jcost (gm / n₂) := by
 124  simp only
 125  have hprod : 0 < n₁ * n₂ := mul_pos hn₁ hn₂
 126  have hgm : 0 < Real.sqrt (n₁ * n₂) := Real.sqrt_pos.mpr hprod
 127  -- gm/n₁ = √(n₂/n₁) and gm/n₂ = √(n₁/n₂) = (√(n₂/n₁))⁻¹
 128  -- Since J(x) = J(1/x), these are equal
 129  have hgm_sq : Real.sqrt (n₁ * n₂) ^ 2 = n₁ * n₂ :=
 130    Real.sq_sqrt (le_of_lt hprod)
 131  -- Use reciprocal symmetry: J(gm/n₁) = J(n₂/gm) = J(gm/n₂) by J(x)=J(1/x)
 132  -- Actually: gm/n₁ = √(n₂/n₁) and gm/n₂ = √(n₁/n₂), and these are reciprocals
 133  have hn₁ne : n₁ ≠ 0 := ne_of_gt hn₁
 134  have hn₂ne : n₂ ≠ 0 := ne_of_gt hn₂
 135  have hgmne : Real.sqrt (n₁ * n₂) ≠ 0 := ne_of_gt hgm
 136  -- Both sides equal J(√(n₂/n₁)) by direct computation.
 137  -- Instead, use the simpler route: both ratios have the same J-value
 138  -- because J depends only on (x - 1)²/(2x), and we can show the
 139  -- squared-form representations are equal.