Documentation

Lean 4 Proof

theorem factorShare_eq_escort {J : ℕ} (ρ : ℝ) (x : Fin J → ℝ) (j : Fin J) :
    factorShare J (fun _ => (1 : ℝ)) ρ x j = escortDistribution J ρ x j := by
  simp [factorShare, escortDistribution]

Dependency Graph

Used by

Location

thesis/CESProofs/Applications/Economics.lean:194

Module Section

Economics extensions for CES formalization:

In the same file