Documentation

Lean 4 Proof

theorem logCES_eq_logPartition [NeZero J] {ρ : ℝ} (hρ : ρ ≠ 0)
    (x : Fin J → ℝ) (hx : ∀ j, 0 < x j) :
    ρ * Real.log (powerMean J ρ hρ x) =
    Real.log (escortPartitionZ x ρ) - Real.log ↑J := by
  have hJ : (0 : ℝ) < ↑J := Nat.cast_pos.mpr (NeZero.pos J)
  have hZ : 0 < escortPartitionZ x ρ := escortPartitionZ_pos x hx ρ
  have hFpos : 0 < powerMean J ρ hρ x := by
    unfold powerMean
    exact rpow_pos_of_pos (mul_pos (div_pos one_pos hJ) hZ) _
  have hid := ces_pow_eq_mean_partition hρ x hx
  have := congr_arg Real.log hid
  rw [Real.log_rpow hFpos] at this
  rw [Real.log_mul (ne_of_gt (div_pos one_pos hJ)) (ne_of_gt hZ)] at this
  rw [Real.log_div one_ne_zero (ne_of_gt hJ), Real.log_one, zero_sub] at this
  linarith

Dependency Graph

Used by

Location

thesis/CESProofs/Foundations/InformationGeometry.lean:901

Module Section

### Part F: The Dual Curvature Principle

In the same file