Documentation

Lean 4 Proof

def factorShare (J : ℕ) (a : Fin J → ℝ) (ρ : ℝ) (x : Fin J → ℝ) (j : Fin J) : ℝ :=
  a j * (x j) ^ ρ / ∑ i : Fin J, a i * (x i) ^ ρ

Dependency Graph

Used by

Location

thesis/CESProofs/Applications/Economics.lean:111

Module Section

Economics extensions for CES formalization:

In the same file