Documentation

Lean 4 Proof

def cesGradComponent (J : ℕ) (ρ : ℝ) (x : Fin J → ℝ) (k : Fin J) : ℝ :=
  (1 / ↑J) * (x k) ^ (ρ - 1) *
    ((1 / ↑J : ℝ) * ∑ j : Fin J, (x j) ^ ρ) ^ ((1 - ρ) / ρ)

Dependency Graph

Used by

Location

thesis/CESProofs/Applications/Economics.lean:683

Module Section

Economics extensions for CES formalization:

In the same file