Documentation

Lean 4 Proof

def cesSlutkyTerm (σ : ℝ) (s : Fin J → ℝ) (j k : Fin J) : ℝ :=
  σ * s j * ((if j = k then 1 else 0) - s k)

Dependency Graph

Used by

Location

thesis/CESProofs/Applications/Economics.lean:885

Module Section

Economics extensions for CES formalization:

In the same file