OAI/Probability/RadialTransition/PressureContinuity.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RadialTransition.grandOn_grid_perturbation line 14
2. lemma OAI.RadialTransition.attractionProfile_mono line 67
3. lemma OAI.RadialTransition.familyPotential_grid_lower line 75
4. lemma OAI.RadialTransition.familyPotential_grid_difference line 85
5. def OAI.RadialTransition.localMomentBound line 114
6. def OAI.RadialTransition.familyPressureLipschitz line 117
7. lemma OAI.RadialTransition.localMomentBound_nonneg line 120
8. lemma OAI.RadialTransition.familyPressureLipschitz_nonneg line 123
9. theorem OAI.RadialTransition.finiteGrandPressure_family_difference line 129
10. lemma OAI.RadialTransition.stable_family_of_master line 187
11. theorem OAI.RadialTransition.grandPressure_family_difference line 197