OAI/Probability/RadialTransition/IdealLimit.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RadialTransition.finiteMax line 12
  2. lemma OAI.RadialTransition.finiteMax_le line 13
  3. lemma OAI.RadialTransition.le_finiteMax line 15
  4. lemma OAI.RadialTransition.finiteMax_attained line 17
  5. def OAI.RadialTransition.phaseMass line 21
  6. def OAI.RadialTransition.phaseDensity line 22
  7. def OAI.RadialTransition.phaseOffset line 23
  8. def OAI.RadialTransition.limitingPlane line 24
  9. def OAI.RadialTransition.threePlane line 26
  10. lemma OAI.RadialTransition.phaseMass_pos line 28
  11. lemma OAI.RadialTransition.phaseDensity_bounds line 30
  12. lemma OAI.RadialTransition.bareLimit_finiteMax line 42
  13. lemma OAI.RadialTransition.limiting_branch_attained line 61
  14. lemma OAI.RadialTransition.limiting_branch_ge line 71
  15. lemma OAI.RadialTransition.limiting_branch_le line 80
  16. lemma OAI.RadialTransition.ideal_approx_threePlane line 89
  17. lemma OAI.RadialTransition.active_near_phase line 110