Documentation

Lean 4 Proof

def manipulationPayoff (J : ℕ) (F : AggFun J) (x : Fin J → ℝ)
    (S : Finset (Fin J)) (δ : Fin J → ℝ)
    (_hδ : ∑ j ∈ S, δ j = 0) : ℝ :=
  F (fun j => x j + if j ∈ S then δ j else 0) - F x

Dependency Graph

Location

thesis/CESProofs/CurvatureRoles/Strategic.lean:23

Module Section

Strategic independence of CES (Paper 1, Sections 7-8):

In the same file