Documentation

Lean 4 Proof

theorem escortPartitionZ_hasDerivAt
    (x : Fin J → ℝ) (hx : ∀ j, 0 < x j) (ρ : ℝ) :
    HasDerivAt (escortPartitionZ x)
      (escortPartitionZ' x ρ) ρ := by
  unfold escortPartitionZ escortPartitionZ'
  convert HasDerivAt.sum (u := Finset.univ)
    (fun j _ => hasDerivAt_rpow_exponent (hx j) ρ)
    using 1
  ext p; simp

Dependency Graph

Used by

Location

thesis/CESProofs/Foundations/InformationGeometry.lean:746

Module Section

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

In the same file