Documentation

Lean 4 Proof

theorem general_bridge_qf (ρ F : ℝ) (P x v : Fin J → ℝ)
    (hx : ∀ j, x j ≠ 0) (hρ : ρ ≠ 0) :
    cesGeneralHessianQF ρ F P x v =
      -((1 - ρ) / ρ ^ 2) * F * escortFisherQF ρ P x v := by
  rw [cesGeneralHessianQF_eq_neg_variance ρ F P x v hx]
  simp only [escortFisherQF]
  have hρ2 : ρ ^ 2 ≠ 0 := pow_ne_zero 2 hρ
  field_simp

Dependency Graph

Location

thesis/CESProofs/Foundations/GeneralHessian.lean:384

Module Section

General CES Hessian at Arbitrary Allocation

In the same file