Documentation

Lean 4 Proof

theorem cesGeneralHessianQF_euler (ρ F : ℝ)
    (P x : Fin J → ℝ)
    (hx : ∀ j, x j ≠ 0) (hP : ∑ j, P j = 1) :
    cesGeneralHessianQF ρ F P x x = 0 := by
  rw [cesGeneralHessianQF_eq_neg_variance ρ F P x x hx]
  have h1 : ∀ k : Fin J, x k / x k = 1 :=
    fun k => div_self (hx k)
  simp_rw [h1, one_pow, mul_one, hP, one_pow,
    sub_self, mul_zero]

Dependency Graph

Location

thesis/CESProofs/Foundations/GeneralHessian.lean:227

Module Section

General CES Hessian at Arbitrary Allocation

In the same file