Documentation

Lean 4 Proof

theorem escort_variance_nonneg [NeZero J]
    (x : Fin J → ℝ) (hx : ∀ j, 0 < x j) (ρ : ℝ)
    (f : Fin J → ℝ) :
    0 ≤ escortVariance x ρ f := by
  unfold escortVariance escortExpectation
  rw [variance_identity _ _ (escort_prob_sum_one x hx ρ)]
  apply Finset.sum_nonneg
  intro j _
  apply mul_nonneg
  · exact div_nonneg (le_of_lt (rpow_pos_of_pos (hx j) ρ))
      (le_of_lt (escortPartitionZ_pos x hx ρ))
  · exact sq_nonneg _

Dependency Graph

Used by

Location

thesis/CESProofs/Foundations/CESEstimation.lean:461

Module Section

CES Estimation Theory: Connecting Theory to Data

In the same file