Documentation

Lean 4 Proof

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

Dependency Graph

Location

thesis/CESProofs/Applications/Economics.lean:224

Module Section

Economics extensions for CES formalization:

In the same file