OAI/MathematicalPhysics/CriticalSK/Equilibrium.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CriticalSK.continuousGoodMass_le_one line 14
  2. lemma OAI.CriticalSK.discreteGoodMass_le_one line 22
  3. lemma OAI.CriticalSK.continuous_bad_subset line 30
  4. lemma OAI.CriticalSK.discrete_bad_subset line 43
  5. lemma OAI.CriticalSK.realized_continuous_initial_states line 56
  6. lemma OAI.CriticalSK.realized_discrete_initial_states line 79
  7. theorem OAI.CriticalSK.realized_equilibrium_initial_states line 103

    Distinct definitions of this name: ComparatorChallenges/CriticalSK.lean:112 (same statement text; different proof or body). Qualify references as OAI.CriticalSK.realized_equilibrium_initial_states@path.