Documentation

Lean 4 Proof

theorem escort_at_symmetry [NeZero J] {c ρ : ℝ} (hc : 0 < c)
    (j : Fin J) :
    escortProbability (fun _ : Fin J => c) ρ j = 1 / ↑J := by
  unfold escortProbability escortPartitionZ
  simp only [Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul]
  have hcr : (c : ℝ) ^ ρ ≠ 0 := ne_of_gt (rpow_pos_of_pos hc ρ)
  have hJ : (↑J : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr (NeZero.ne J)
  field_simp

Dependency Graph

Location

thesis/CESProofs/Foundations/InformationGeometry.lean:962

Module Section

### Part F: The Dual Curvature Principle

In the same file