Documentation

Lean 4 Proof

theorem escortFisherQF_nonneg (ρ : ℝ) (P x v : Fin J → ℝ)
    (hP_nn : ∀ j, 0 ≤ P j) (hP_sum : ∑ j, P j = 1) :
    0 ≤ escortFisherQF ρ P x v := by
  simp only [escortFisherQF]
  apply mul_nonneg (sq_nonneg ρ)
  exact weighted_variance_nonneg P (fun j => v j / x j) hP_nn hP_sum

Dependency Graph

Location

thesis/CESProofs/Foundations/GeneralHessian.lean:394

Module Section

General CES Hessian at Arbitrary Allocation

In the same file