arithmeticMean

formal source

 154/-! ## §4. Simultaneous vs sequential descent -/
 155
 156/-- **F1.4.2**: The arithmetic mean of two positive reals -/
 157noncomputable def arithmeticMean (n₁ n₂ : ℝ) : ℝ := (n₁ + n₂) / 2
 158
 159/-- **F1.4.3**: For distinct positive reals, the geometric mean differs
 160    from the arithmetic mean (AM-GM strict inequality). -/
 161theorem geometric_ne_arithmetic {n₁ n₂ : ℝ} (hn₁ : 0 < n₁) (hn₂ : 0 < n₂)
 162    (hne : n₁ ≠ n₂) :
 163    Real.sqrt (n₁ * n₂) ≠ (n₁ + n₂) / 2 := by
 164  intro h
 165  -- If √(n₁n₂) = (n₁+n₂)/2, squaring gives n₁n₂ = (n₁+n₂)²/4
 166  -- i.e. 4n₁n₂ = (n₁+n₂)² = n₁² + 2n₁n₂ + n₂²
 167  -- i.e. 0 = n₁² - 2n₁n₂ + n₂² = (n₁-n₂)²
 168  -- contradicting n₁ ≠ n₂
 169  have hprod : 0 ≤ n₁ * n₂ := le_of_lt (mul_pos hn₁ hn₂)
 170  have hsum_pos : 0 < (n₁ + n₂) / 2 := by linarith
 171  have hsq : n₁ * n₂ = ((n₁ + n₂) / 2) ^ 2 := by
 172    have h2 : Real.sqrt (n₁ * n₂) ^ 2 = n₁ * n₂ := Real.sq_sqrt hprod
 173    rw [← h2, h]
 174  have : (n₁ - n₂) ^ 2 = 0 := by nlinarith [hsq]
 175  have : n₁ - n₂ = 0 := by
 176    exact_mod_cast sq_eq_zero_iff.mp this
 177  exact hne (by linarith)
 178
 179/-- **Key structural fact**: Sequential single-bond descent (take v = n₁, then v = n₂,
 180    etc.) converges toward the arithmetic mean, while simultaneous descent converges
 181    to the geometric mean. The two differ for distinct neighbors. -/
 182theorem simultaneous_differs_from_sequential {n₁ n₂ : ℝ}
 183    (hn₁ : 0 < n₁) (hn₂ : 0 < n₂) (hne : n₁ ≠ n₂) :
 184    Real.sqrt (n₁ * n₂) ≠ arithmeticMean n₁ n₂ :=
 185  geometric_ne_arithmetic hn₁ hn₂ hne
 186
 187/-! ## §5. Derived identities -/