OAI/Probability/ContinuumTransition/CanonicalIntegral.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ContinuumTemperature.radialPotential_ne_bot line 13
2. theorem OAI.ContinuumTemperature.ereal_sum_ne_bot line 20
3. theorem OAI.ContinuumTemperature.measurable_energy line 29
4. theorem OAI.ContinuumTemperature.measurable_boltzmann line 35
5. theorem OAI.ContinuumTemperature.boltzmann_nonneg line 41
6. theorem OAI.ContinuumTemperature.boltzmann_le_of_stable line 48
7. theorem OAI.ContinuumTemperature.isCompact_cube line 61
8. theorem OAI.ContinuumTemperature.measurableSet_cube line 65
9. theorem OAI.ContinuumTemperature.isCompact_configurations line 68
10. theorem OAI.ContinuumTemperature.integrableOn_boltzmann line 72
11. theorem OAI.ContinuumTemperature.energy_eq_real_of_injective line 88
12. theorem OAI.ContinuumTemperature.boltzmann_pos_of_injective line 102
13. def OAI.ContinuumTemperature.openConfigurations line 108
14. theorem OAI.ContinuumTemperature.isOpen_openConfigurations line 111
15. theorem OAI.ContinuumTemperature.openConfigurations_nonempty line 137
16. theorem OAI.ContinuumTemperature.partition_pos line 158
17. theorem OAI.ContinuumTemperature.boltzmann_add line 177
18. theorem OAI.ContinuumTemperature.boltzmann_rpow line 186
19. theorem OAI.ContinuumTemperature.integral_boltzmann_logconvex line 196
20. theorem OAI.ContinuumTemperature.integral_boltzmann_pos line 240
21. theorem OAI.ContinuumTemperature.convexOn_log_integral_boltzmann line 255
22. theorem OAI.ContinuumTemperature.convexOn_log_partition line 276
23. theorem OAI.ContinuumTemperature.volume_cube line 302
24. theorem OAI.ContinuumTemperature.volume_configurations line 315
25. theorem OAI.ContinuumTemperature.partition_nonneg line 324
26. theorem OAI.ContinuumTemperature.partition_le_exp_of_stable line 332