OAI/Probability/ContinuumTransition/GenericGibbs.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ContinuumTemperature.gibbsEnergy line 11
2. def OAI.ContinuumTemperature.gibbsFamily line 15
3. def OAI.ContinuumTemperature.occupation line 18
4. theorem OAI.ContinuumTemperature.occupation_nonneg line 21
5. theorem OAI.ContinuumTemperature.occupation_eq_sum line 24
6. theorem OAI.ContinuumTemperature.measurable_occupation line 29
7. theorem OAI.ContinuumTemperature.occupation_relabel line 37
8. theorem OAI.ContinuumTemperature.occupation_subtype_compl line 43
9. theorem OAI.ContinuumTemperature.gibbsEnergy_relabel line 59
10. theorem OAI.ContinuumTemperature.gibbsFamily_relabel line 70
11. theorem OAI.ContinuumTemperature.gibbsFamily_nonneg line 82
12. theorem OAI.ContinuumTemperature.gibbsEnergy_split line 89
13. theorem OAI.ContinuumTemperature.measurable_gibbsEnergy line 107
14. theorem OAI.ContinuumTemperature.measurableSet_injective_config line 124
15. theorem OAI.ContinuumTemperature.measurable_gibbsFamily line 144
16. def OAI.ContinuumTemperature.momentFamily line 150
17. theorem OAI.ContinuumTemperature.momentFamily_relabel line 153
18. theorem OAI.ContinuumTemperature.momentFamily_nonneg line 158
19. theorem OAI.ContinuumTemperature.measurable_momentFamily line 163
20. theorem OAI.ContinuumTemperature.gibbs_moment_stable_bound line 168
21. theorem OAI.ContinuumTemperature.gibbs_moment_insertion line 180