Documentation

Lean 4 Proof

theorem escortFisherQF_zero_radial (ρ : ℝ) (P x : Fin J → ℝ)
    (hx : ∀ j, x j ≠ 0) (hP : ∑ j, P j = 1) :
    escortFisherQF ρ P x x = 0 := by
  simp only [escortFisherQF]
  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:405

Module Section

General CES Hessian at Arbitrary Allocation

In the same file