Documentation

Lean 4 Proof

def AxiomA4_LogitRecovery (T : ℝ) : Prop :=
  T > 0  -- simplified: the logit is well-defined for T > 0

Dependency Graph

Location

thesis/CESProofs/Potential/CESPotential.lean:60

Module Section

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

In the same file