OAI/Probability/RadialTransition/TruncatedFamily.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RadialTransition.reversePrefix line 10
  2. lemma OAI.RadialTransition.reversePrefix_zero line 13
  3. lemma OAI.RadialTransition.reversePrefix_succ line 14
  4. lemma OAI.RadialTransition.reversePrefix_nonneg line 16
  5. lemma OAI.RadialTransition.reversePrefix_range line 20
  6. lemma OAI.RadialTransition.reversePrefix_range_le line 24
  7. lemma OAI.RadialTransition.summable_reversePrefix line 33
  8. lemma OAI.RadialTransition.tsum_reversePrefix line 37
  9. lemma OAI.RadialTransition.attractionProfile_reversePrefix line 42
  10. def OAI.RadialTransition.cutMass line 51
  11. lemma OAI.RadialTransition.cutMass_nonneg line 52
  12. lemma OAI.RadialTransition.cutMass_le line 56
  13. lemma OAI.RadialTransition.summable_cutMass line 58
  14. lemma OAI.RadialTransition.tsum_cutMass line 63
  15. lemma OAI.RadialTransition.attractionProfile_cutMass line 68
  16. lemma OAI.RadialTransition.familyPotential_reverse_cut line 75
  17. lemma OAI.RadialTransition.reversePrefix_admissible line 80
  18. lemma OAI.RadialTransition.cutMass_difference line 86
  19. lemma OAI.RadialTransition.tendsto_cutMass_difference line 92
  20. lemma OAI.RadialTransition.grandPressure_reversePrefix_tendsto line 96