The arithmetic-geometric mean

Starting with two nonnegative real numbers, repeatedly replace them with their arithmetic and geometric means. By the AM-GM inequality, the smaller number (geometric mean) will monotonically increase and the larger number (arithmetic mean) will monotonically decrease.

The two monotone sequences converge to the same limit – the arithmetic-geometric mean (AGM). This file defines the AGM in the NNReal namespace and proves some of its basic properties.

References

• https://en.wikipedia.org/wiki/Arithmetic–geometric_mean

theorem NNReal.sqrt_mul_le_half_add (x y : NNReal) : sqrt (x * y) ≤ (x + y) / 2

The AM–GM inequality for two NNReals, with means in canonical form.

theorem NNReal.sqrt_mul_lt_half_add_of_ne {x y : NNReal} (h : x ≠ y) : sqrt (x * y) < (x + y) / 2

The strict AM–GM inequality for two NNReals, with means in canonical form.

noncomputable def NNReal.agmSequences (x y : NNReal) : ℕ → NNReal × NNReal

agmSequences x y is the sequence of (geometric, arithmetic) means converging to the arithmetic-geometric mean starting from x and y.

@[simp]

theorem NNReal.agmSequences_zero {x y : NNReal} : x.agmSequences y 0 = (sqrt (x * y), (x + y) / 2)

theorem NNReal.agmSequences_succ {x y : NNReal} {n : ℕ} : x.agmSequences y (n + 1) = (sqrt (x * y)).agmSequences ((x + y) / 2) n

theorem NNReal.agmSequences_succ' {x y : NNReal} {n : ℕ} : x.agmSequences y (n + 1) = (sqrt ((x.agmSequences y n).1 * (x.agmSequences y n).2), ((x.agmSequences y n).1 + (x.agmSequences y n).2) / 2)

theorem NNReal.agmSequences_comm {x y : NNReal} : x.agmSequences y = y.agmSequences x

theorem NNReal.le_gm_and_am_le {x y : NNReal} (h : x ≤ y) : x ≤ sqrt (x * y) ∧ (x + y) / 2 ≤ y

theorem NNReal.dist_gm_am_le {x y : NNReal} : dist (sqrt (x * y)) ((x + y) / 2) ≤ dist x y / 2

theorem NNReal.agmSequences_monotone_and_antitone {x y : NNReal} : (Monotone fun (n : ℕ) => (x.agmSequences y n).1) ∧ Antitone fun (n : ℕ) => (x.agmSequences y n).2

theorem NNReal.agmSequences_fst_monotone {x y : NNReal} : Monotone fun (n : ℕ) => (x.agmSequences y n).1

theorem NNReal.agmSequences_snd_antitone {x y : NNReal} : Antitone fun (n : ℕ) => (x.agmSequences y n).2

theorem NNReal.agmSequences_fst_le_snd {x y : NNReal} (n m : ℕ) : (x.agmSequences y n).1 ≤ (x.agmSequences y m).2

theorem NNReal.agmSequences_fst_lt_snd_of_ne {x y : NNReal} (h : x ≠ y) (n m : ℕ) : (x.agmSequences y n).1 < (x.agmSequences y m).2

theorem NNReal.agmSequences_min_max {x y : NNReal} : (min x y).agmSequences (max x y) = x.agmSequences y

theorem NNReal.dist_agmSequences_fst_snd {x y : NNReal} (n : ℕ) : dist (x.agmSequences y n).1 (x.agmSequences y n).2 ≤ dist x y / 2 ^ (n + 1)

theorem NNReal.tendsto_dist_agmSequences_atTop_zero {x y : NNReal} : Filter.Tendsto (fun (n : ℕ) => dist (x.agmSequences y n).1 (x.agmSequences y n).2) Filter.atTop (nhds 0)

noncomputable def NNReal.agm (x y : NNReal) : NNReal

The arithmetic-geometric mean of two NNReals, defined as the infimum of arithmetic means.

theorem NNReal.agm_comm {x y : NNReal} : x.agm y = y.agm x

theorem NNReal.agm_eq_ciInf {x y : NNReal} : x.agm y = ⨅ (n : ℕ), (x.agmSequences y n).2

theorem NNReal.tendsto_agmSequences_snd_agm {x y : NNReal} : Filter.Tendsto (fun (n : ℕ) => (x.agmSequences y n).2) Filter.atTop (nhds (x.agm y))

theorem NNReal.agm_le_agmSequences_snd {x y : NNReal} (n : ℕ) : x.agm y ≤ (x.agmSequences y n).2

theorem NNReal.agm_le_max {x y : NNReal} : x.agm y ≤ max x y

theorem NNReal.bddAbove_range_agmSequences_fst {x y : NNReal} : BddAbove (Set.range fun (n : ℕ) => (x.agmSequences y n).1)

theorem NNReal.agm_eq_ciSup {x y : NNReal} : x.agm y = ⨆ (n : ℕ), (x.agmSequences y n).1

The AGM is also the supremum of the geometric means.

theorem NNReal.tendsto_agmSequences_fst_agm {x y : NNReal} : Filter.Tendsto (fun (n : ℕ) => (x.agmSequences y n).1) Filter.atTop (nhds (x.agm y))

theorem NNReal.agmSequences_fst_le_agm {x y : NNReal} (n : ℕ) : (x.agmSequences y n).1 ≤ x.agm y

theorem NNReal.min_le_agm {x y : NNReal} : min x y ≤ x.agm y

@[simp]

theorem NNReal.agm_self {x : NNReal} : x.agm x = x

@[simp]

theorem NNReal.agm_zero_left {y : NNReal} : agm 0 y = 0

@[simp]

theorem NNReal.agm_zero_right {x : NNReal} : x.agm 0 = 0

theorem NNReal.agm_pos {x y : NNReal} (hx : 0 < x) (hy : 0 < y) : 0 < x.agm y

theorem NNReal.agm_eq_agm_agmSequences_fst_agmSequences_snd {x y : NNReal} (n : ℕ) : x.agm y = (x.agmSequences y n).1.agm (x.agmSequences y n).2

theorem NNReal.agm_eq_agm_gm_am {x y : NNReal} : x.agm y = (sqrt (x * y)).agm ((x + y) / 2)

theorem NNReal.agmSequences_fst_lt_agm_of_pos_of_ne {x y : NNReal} (hx : 0 < x) (hy : 0 < y) (hn : x ≠ y) (n : ℕ) : (x.agmSequences y n).1 < x.agm y

theorem NNReal.agm_lt_agmSequences_snd_of_ne {x y : NNReal} (hn : x ≠ y) (n : ℕ) : x.agm y < (x.agmSequences y n).2

theorem NNReal.min_lt_agm_of_pos_of_ne {x y : NNReal} (hx : 0 < x) (hy : 0 < y) (hn : x ≠ y) : min x y < x.agm y

theorem NNReal.agm_lt_max_of_ne {x y : NNReal} (hn : x ≠ y) : x.agm y < max x y

theorem NNReal.agm_mul_distrib {x y k : NNReal} : (k * x).agm (k * y) = k * x.agm y

The AGM distributes over multiplication.