Documentation

Lean 4 Proof

theorem escortPartitionZ'_hasDerivAt
    (x : Fin J → ℝ) (hx : ∀ j, 0 < x j) (ρ : ℝ) :
    HasDerivAt (escortPartitionZ' x)
      (∑ j, x j ^ ρ * (Real.log (x j)) ^ 2) ρ := by
  unfold escortPartitionZ'
  convert HasDerivAt.sum (u := Finset.univ)
    (fun j _ => hasDerivAt_rpow_exponent_sq (hx j) ρ)
    using 1
  ext p; simp

Dependency Graph

Location

thesis/CESProofs/Foundations/InformationGeometry.lean:757

Module Section

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

In the same file