Documentation

Lean 4 Proof

def genCesHessianQF (J : ℕ) (ρ : ℝ) (a : Fin J → ℝ) (c : ℝ)
    (v : Fin J → ℝ) : ℝ :=
  let σ := 1 / (1 - ρ)
  let p := fun j => (a j) ^ σ
  (1 - ρ) / c * ((∑ j : Fin J, v j) ^ 2 / (∑ j, p j) -
                   ∑ j : Fin J, (v j) ^ 2 / p j)

Dependency Graph

Location

thesis/CESProofs/Foundations/GeneralWeights.lean:62

Module Section

General-weight CES results (Paper 1, Section 10):

In the same file