OAI/Probability/ContinuumTransition/ConstructionMasses.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ContinuumTemperature.ConstructionData.masses line 11
  2. def OAI.ContinuumTemperature.prefixMass line 13
  3. def OAI.ContinuumTemperature.tailMass line 15
  4. lemma OAI.ContinuumTemperature.prefixMass_nonneg line 17
  5. lemma OAI.ContinuumTemperature.tailMass_nonneg line 23
  6. lemma OAI.ContinuumTemperature.prefixMass_add_tailMass line 29
  7. lemma OAI.ContinuumTemperature.prefixMass_summable line 36
  8. lemma OAI.ContinuumTemperature.tailMass_summable line 43
  9. lemma OAI.ContinuumTemperature.tsum_prefixMass line 50
  10. lemma OAI.ContinuumTemperature.tailMass_tsum_tendsto line 59
  11. lemma OAI.ContinuumTemperature.ConstructionData.reference_mass line 68
  12. lemma OAI.ContinuumTemperature.ConstructionData.masses_nonneg line 77
  13. lemma OAI.ContinuumTemperature.ConstructionData.sum_masses_le line 80
  14. lemma OAI.ContinuumTemperature.ConstructionData.masses_summable line 85
  15. lemma OAI.ContinuumTemperature.ConstructionData.mass_bound line 88
  16. lemma OAI.ContinuumTemperature.ConstructionData.ranges_one line 91
  17. lemma OAI.ContinuumTemperature.ConstructionData.reference_profile line 95
  18. lemma OAI.ContinuumTemperature.attraction_prefixMass line 107
  19. lemma OAI.ContinuumTemperature.ConstructionData.reference_eq_prefix line 118