OAI/Probability/SKSupport/Support/GapCurvature.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ZeroTemperatureSK.OrderParameter.continuousAt_of_constant line 14
2. lemma OAI.ZeroTemperatureSK.compactCoeff_constant line 23
3. lemma OAI.ZeroTemperatureSK.curvatureMoment_hasDerivAt_on_constant line 30
4. lemma OAI.ZeroTemperatureSK.curvatureMoment_deriv_hasDerivAt_on_constant line 39
5. theorem OAI.ZeroTemperatureSK.positive_gap_curvature line 48
6. theorem OAI.ZeroTemperatureSK.zero_gap_curvature line 63
7. instance OAI.ZeroTemperatureSK.timeCompactIccSpace line 83
8. def OAI.ZeroTemperatureSK.parameterStieltjes line 96
9. lemma OAI.ZeroTemperatureSK.parameterStieltjes_atBot line 101
10. def OAI.ZeroTemperatureSK.parameterMeasure line 109
11. lemma OAI.ZeroTemperatureSK.parameterMeasure_isStieltjes line 112