OAI/Probability/ContinuumTransition/LowerEnergy.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ContinuumTemperature.occupation_disjoint_eq_fiber line 11
2. theorem OAI.ContinuumTemperature.card_eq_sum_fibers line 27
3. theorem OAI.ContinuumTemperature.kacLower_grid_double_lower line 32
4. theorem OAI.ContinuumTemperature.kac_energy_lower_fixed line 51