Documentation

Lean 4 Proof

theorem fisherInfoRho_nonneg [NeZero J]
    (x : Fin J → ℝ) (hx : ∀ j, 0 < x j) (ρ : ℝ) :
    0 ≤ fisherInfoRho x ρ :=
  escort_variance_nonneg x hx ρ _

Dependency Graph

Location

thesis/CESProofs/Foundations/CESEstimation.lean:476

Module Section

CES Estimation Theory: Connecting Theory to Data

In the same file