OAI/Probability/SKSupport/Support/CDFParameters.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ZeroTemperatureSK.extend_add_fun line 14
2. lemma OAI.ZeroTemperatureSK.extend_sub_fun line 17
3. def OAI.ZeroTemperatureSK.OrderParameter.addCDF line 21
4. lemma OAI.ZeroTemperatureSK.OrderParameter.addCDF_difference line 28
5. lemma OAI.ZeroTemperatureSK.stieltjes_real line 34
6. lemma OAI.ZeroTemperatureSK.finiteCDF_le_parameter line 37
7. lemma OAI.ZeroTemperatureSK.cdf_real_add_Ioc line 44
8. lemma OAI.ZeroTemperatureSK.removeCDF_monotone line 54
9. def OAI.ZeroTemperatureSK.OrderParameter.removeCDF line 66
10. lemma OAI.ZeroTemperatureSK.OrderParameter.removeCDF_difference line 74
11. lemma OAI.ZeroTemperatureSK.OrderParameter.original_deterministic line 81
12. lemma OAI.ZeroTemperatureSK.stieltjes_deterministic line 102
13. lemma OAI.ZeroTemperatureSK.finiteCDF_fubini line 117