OAI/Geometry/CAT0Fillings/Rearrangement/Distribution.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CAT0Fillings.Rearrangement.negativeTail line 13
2. lemma OAI.CAT0Fillings.Rearrangement.negativeTail_measure line 23
3. lemma OAI.CAT0Fillings.Rearrangement.ae_hasDerivAt_tail line 48
4. lemma OAI.CAT0Fillings.Rearrangement.stieltjes_secant_lower line 58
5. def OAI.CAT0Fillings.Rearrangement.radiusDistribution line 91
6. lemma OAI.CAT0Fillings.Rearrangement.radius_nonneg line 96
7. lemma OAI.CAT0Fillings.Rearrangement.radius_pos line 100
8. lemma OAI.CAT0Fillings.Rearrangement.radius_pow line 103
9. lemma OAI.CAT0Fillings.Rearrangement.radius_antitone line 111
10. lemma OAI.CAT0Fillings.Rearrangement.radius_right_continuous line 117
11. def OAI.CAT0Fillings.Rearrangement.negativeRadius line 126
12. lemma OAI.CAT0Fillings.Rearrangement.ae_radius_derivative line 131
13. lemma OAI.CAT0Fillings.Rearrangement.radius_secant_from_coarea line 147