Documentation

Lean 4 Proof

theorem escort_variance_const [NeZero J]
    (x : Fin J → ℝ) (hx : ∀ j, 0 < x j) (ρ : ℝ) (c : ℝ) :
    escortVariance x ρ (fun _ => c) = 0 := by
  unfold escortVariance
  rw [show (fun j : Fin J => (fun _ => c) j ^ 2) = (fun _ => c ^ 2) from rfl]
  rw [escort_expectation_const x hx ρ (c ^ 2),
      escort_expectation_const x hx ρ c]
  ring

Dependency Graph

Used by

Location

thesis/CESProofs/Foundations/InformationGeometry.lean:947

Module Section

### Part F: The Dual Curvature Principle

In the same file