OAI/Probability/ContinuumTransition/GeneralGrand.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ContinuumTemperature.ConfigFamily line 10
  2. def OAI.ContinuumTemperature.RelabelInvariant line 12
  3. def OAI.ContinuumTemperature.familyIntegral line 16
  4. def OAI.ContinuumTemperature.familyTerm line 20
  5. def OAI.ContinuumTemperature.grandIntegral line 23
  6. theorem OAI.ContinuumTemperature.familyIntegral_relabel line 26
  7. theorem OAI.ContinuumTemperature.familyIntegral_eq_Fin line 50
  8. theorem OAI.ContinuumTemperature.integral_binary_bound line 55
  9. theorem OAI.ContinuumTemperature.factorial_binomial_sum line 76
  10. theorem OAI.ContinuumTemperature.familyTerm_nonneg line 86
  11. theorem OAI.ContinuumTemperature.integrableOn_family_of_bound line 92
  12. theorem OAI.ContinuumTemperature.familyTerm_le_exponential line 107
  13. theorem OAI.ContinuumTemperature.summable_familyTerm_of_bound line 127
  14. theorem OAI.ContinuumTemperature.tsum_le_convolution line 137
  15. theorem OAI.ContinuumTemperature.grandIntegral_insertion_bound line 146