Documentation

Lean 4 Proof

theorem escort_vri [NeZero J] (x : Fin J → ℝ)
    (hx : ∀ j, 0 < x j) (ρ : ℝ) :
    HasDerivAt
      (fun p => escortPartitionZ' x p
        / escortPartitionZ x p)
      (escortVariance x ρ
        (fun j => Real.log (x j))) ρ := by
  have hquot :=
    (escortPartitionZ'_hasDerivAt x hx ρ).div
    (escortPartitionZ_hasDerivAt x hx ρ)
    (ne_of_gt (escortPartitionZ_pos x hx ρ))
  convert hquot using 1
  unfold escortVariance
  rw [escortExpectation_eq_sum_div x hx ρ
    (fun j => Real.log (x j) ^ 2)]
  rw [escortExpectation_eq_sum_div x hx ρ
    (fun j => Real.log (x j))]
  exact (quotient_rule_variance_eq _ _ _
    (ne_of_gt (escortPartitionZ_pos x hx ρ))).symm

Dependency Graph

Location

thesis/CESProofs/Foundations/InformationGeometry.lean:817

Module Section

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

In the same file