OAI/Probability/RadialTransition/IdealAttraction.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.RadialTransition.Pressure line 12
  2. def OAI.RadialTransition.pressureSupport line 14
  3. def OAI.RadialTransition.attractionBranch line 18
  4. def OAI.RadialTransition.idealAttraction line 21
  5. def OAI.RadialTransition.ActiveShift line 24
  6. theorem OAI.RadialTransition.active_parabola line 27
  7. theorem OAI.RadialTransition.active_support_density line 46
  8. theorem OAI.RadialTransition.support_attractionBranch line 65
  9. theorem OAI.RadialTransition.idealAttraction_eq_of_active line 74
  10. theorem OAI.RadialTransition.active_generator_support line 80
  11. theorem OAI.RadialTransition.support_of_attractionBranch line 93