OAI/Probability/ContinuumTransition/GrandDomination.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.ContinuumTemperature.GrandFinite.of_le line 10
  2. theorem OAI.ContinuumTemperature.square_product_le_exponentials line 23
  3. def OAI.ContinuumTemperature.occupationPairFamily line 30
  4. theorem OAI.ContinuumTemperature.occupationPairFamily_nonneg line 33
  5. theorem OAI.ContinuumTemperature.occupationPairFamily_le line 39
  6. theorem OAI.ContinuumTemperature.GrandFinite.occupationPair line 47
  7. theorem OAI.ContinuumTemperature.grand_pair_moment_le line 58