Documentation

Lean 4 Proof

theorem strategic_independence_qualitative (hJ : 2 ≤ J) {ρ : ℝ} (hρ : ρ < 1)
    {c : ℝ} (hc : 0 < c)
    (δ : Fin J → ℝ) (hδ : orthToOne J δ)
    (hδ_ne : ∃ j, δ j ≠ 0) :
    -- The second-order approximation of the manipulation payoff is negative
    cesHessianQF J ρ c δ < 0 :=
  ces_strict_concavity_on_perp hJ hρ hc δ hδ hδ_ne

Dependency Graph

Location

thesis/CESProofs/CurvatureRoles/Strategic.lean:54

Module Section

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

In the same file