OAI/Probability/RadialTransition/ParameterPressure.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.RadialTransition.Parameter line 12
2. def OAI.RadialTransition.parameter line 13
3. def OAI.RadialTransition.positiveParameters line 14
4. def OAI.RadialTransition.onParameters line 15
5. lemma OAI.RadialTransition.parameter_zero line 17
6. lemma OAI.RadialTransition.parameter_one line 18
7. lemma OAI.RadialTransition.parameter_eta line 19
8. lemma OAI.RadialTransition.parameter_inner line 23
9. lemma OAI.RadialTransition.parameter_coord_abs_le line 26
10. lemma OAI.RadialTransition.parameter_norm_le line 29
11. lemma OAI.RadialTransition.continuous_parameter line 36
12. lemma OAI.RadialTransition.isOpen_positiveParameters line 45
13. lemma OAI.RadialTransition.convex_positiveParameters line 48
14. lemma OAI.RadialTransition.pressureSupport_iff line 57
15. lemma OAI.RadialTransition.convexOn_grandPressure line 68
16. lemma OAI.RadialTransition.convexOn_attractionBranch line 76
17. lemma OAI.RadialTransition.convexOn_idealAttraction line 91