OAI/Probability/ContinuumTransition/CanonicalLimit.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ContinuumTemperature.finiteCanonical line 10
  2. theorem OAI.ContinuumTemperature.finiteCanonical_zero line 13
  3. theorem OAI.ContinuumTemperature.finiteCanonical_lower_constant line 16
  4. theorem OAI.ContinuumTemperature.finiteCanonical_upper_trial line 33
  5. theorem OAI.ContinuumTemperature.finiteCanonical_densityBounded line 50
  6. theorem OAI.ContinuumTemperature.finiteCanonical_hasBoxInequality line 81
  7. theorem OAI.ContinuumTemperature.exists_canonical_density_limit line 104
  8. theorem OAI.ContinuumTemperature.finiteCanonical_lower_entropy line 115
  9. theorem OAI.ContinuumTemperature.finiteCanonical_tendsto_zero_density line 131
  10. def OAI.ContinuumTemperature.canonicalDensity line 160
  11. theorem OAI.ContinuumTemperature.finiteCanonical_tendsto line 163
  12. theorem OAI.ContinuumTemperature.canonicalDensity_zero line 178
  13. def OAI.ContinuumTemperature.canonicalFreeEnergy line 186
  14. theorem OAI.ContinuumTemperature.hasCanonicalFreeEnergy_of_core line 189
  15. theorem OAI.ContinuumTemperature.concaveOn_canonicalDensity line 206