Documentation

Lean 4 Proof

theorem escort_first_cumulant [NeZero J]
    (x : Fin J → ℝ) (hx : ∀ j, 0 < x j) (ρ : ℝ) :
    HasDerivAt
      (fun p => Real.log (escortPartitionZ x p))
      (escortExpectation x ρ
        (fun j => Real.log (x j))) ρ := by
  have hA := (escortPartitionZ_hasDerivAt x hx ρ).log
    (ne_of_gt (escortPartitionZ_pos x hx ρ))
  convert hA using 1
  unfold escortExpectation escortProbability
    escortPartitionZ'
  simp_rw [div_mul_eq_mul_div]
  rw [← Finset.sum_div]

Dependency Graph

Location

thesis/CESProofs/Foundations/InformationGeometry.lean:790

Module Section

The VRI σ² = T·χ is fundamentally an exponential family identity:

In the same file