OAI/Probability/RadialTransition/PhaseGeometry.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RadialTransition.phaseSlope_zero line 10
  2. lemma OAI.RadialTransition.phaseSlope_one line 11
  3. lemma OAI.RadialTransition.phaseSlope_two line 17
  4. lemma OAI.RadialTransition.phase_densities_separated line 24
  5. def OAI.RadialTransition.phaseRadius line 30
  6. def OAI.RadialTransition.pressureRadius line 31
  7. lemma OAI.RadialTransition.phaseRadius_pos line 32
  8. lemma OAI.RadialTransition.pressureRadius_pos line 33
  9. lemma OAI.RadialTransition.phaseRadius_lt line 34
  10. def OAI.RadialTransition.directionalMax line 36
  11. lemma OAI.RadialTransition.directional_lower line 38
  12. lemma OAI.RadialTransition.mem_closedHull_of_inner_le line 76
  13. lemma OAI.RadialTransition.robust_phase_triangle line 91
  14. def OAI.RadialTransition.exclusionNormal line 112
  15. lemma OAI.RadialTransition.exclusionNormal_norm line 114
  16. lemma OAI.RadialTransition.exclusion_gap line 118
  17. lemma OAI.RadialTransition.exclusion_ball line 126
  18. lemma OAI.RadialTransition.phase_plane_at_center line 137
  19. lemma OAI.RadialTransition.phase_plane_difference line 141
  20. lemma OAI.RadialTransition.threePlane_center line 148
  21. lemma OAI.RadialTransition.threePlane_growth line 158