Sections / Section 9: CES Potential and Information Friction / AxiomA2_PseudoAdditivePenalty

Axiom A2 Pseudo Additive Penalty

defprovedCES Potential

Documentation

Lean 4 Proof

def AxiomA2_PseudoAdditivePenalty (q : ℝ) : Prop :=
  PseudoAdditive tsallisEntropy q

Dependency Graph

Location

thesis/CESProofs/Potential/CESPotential.lean:44

Module Section

Theorem 3: CES Potential Uniqueness (Paper 2, Section 3.2)

In the same file

AxiomA1_LinearPayoff AxiomA3_Symmetry AxiomA4_LogitRecovery cesPotential_uniqueness cesPotential_affine_in_T cesPotential_zero_friction cesPotential_symmetric cesPotential_eq_effectiveCESPotential