Documentation

Lean 4 Proof

theorem ces_pow_eq_mean_partition [NeZero J] {ρ : ℝ} (hρ : ρ ≠ 0)
    (x : Fin J → ℝ) (hx : ∀ j, 0 < x j) :
    powerMean J ρ hρ x ^ ρ = (1 / ↑J) * escortPartitionZ x ρ := by
  unfold powerMean escortPartitionZ
  have hJ : (0 : ℝ) < ↑J := Nat.cast_pos.mpr (NeZero.pos J)
  have hsum : 0 < ∑ j : Fin J, x j ^ ρ :=
    sum_pos (fun j _ => rpow_pos_of_pos (hx j) ρ) Finset.univ_nonempty
  have hbase : 0 ≤ 1 / ↑J * ∑ j : Fin J, x j ^ ρ :=
    le_of_lt (mul_pos (div_pos one_pos hJ) hsum)
  rw [← rpow_mul hbase, show (1 : ℝ) / ρ * ρ = 1 from by field_simp, rpow_one]

Dependency Graph

Used by

Location

thesis/CESProofs/Foundations/InformationGeometry.lean:879

Module Section

### Part F: The Dual Curvature Principle

In the same file