Documentation

Lean 4 Proof

theorem cesGeneralHessianQF_neg_semidef
    {ρ : ℝ} (hρ : ρ < 1) {F : ℝ} (hF : 0 < F)
    (P : Fin J → ℝ)
    (hP_nn : ∀ j, 0 ≤ P j)
    (hP_sum : ∑ j, P j = 1)
    (x v : Fin J → ℝ) (hx : ∀ j, x j ≠ 0) :
    cesGeneralHessianQF ρ F P x v ≤ 0 := by
  rw [cesGeneralHessianQF_eq_neg_variance ρ F P x v hx]
  have hvar := weighted_variance_nonneg P
    (fun j => v j / x j) hP_nn hP_sum
  have h1 : 0 < (1 - ρ) * F := mul_pos (by linarith) hF
  nlinarith

Dependency Graph

Location

thesis/CESProofs/Foundations/GeneralHessian.lean:209

Module Section

General CES Hessian at Arbitrary Allocation

In the same file