Documentation

Lean 4 Proof

theorem escortPartitionZ_pos [NeZero J]
    (x : Fin J → ℝ) (hx : ∀ j, 0 < x j) (ρ : ℝ) :
    0 < escortPartitionZ x ρ := by
  unfold escortPartitionZ
  exact sum_pos (fun j _ => rpow_pos_of_pos (hx j) ρ)
    Finset.univ_nonempty

Dependency Graph

Used by

Location

thesis/CESProofs/Foundations/InformationGeometry.lean:738

Module Section

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

In the same file