Documentation

Lean 4 Proof

theorem shares_are_expectations_not_sufficient
    [NeZero J] (x : Fin J → ℝ) (_hx : ∀ j, 0 < x j) (ρ : ℝ) :
    -- The escort expectation of log x equals the mean log-input
    -- weighted by the escort probabilities (share-weighted mean).
    escortExpectation x ρ (fun j => Real.log (x j)) =
    ∑ j, escortProbability x ρ j * Real.log (x j) := by
  rfl

Dependency Graph

Location

thesis/CESProofs/Foundations/CESEstimation.lean:195

Module Section

CES Estimation Theory: Connecting Theory to Data

In the same file