OAI/Geometry/CAT0Fillings/BV/Oscillation.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CAT0Fillings.JointBV.abs_setAverage_sub_le line 13
2. lemma OAI.CAT0Fillings.JointBV.abs_setAverage_sub_le_integral line 32
3. lemma OAI.CAT0Fillings.JointBV.haar_closedBall_pos line 50
4. lemma OAI.CAT0Fillings.JointBV.haar_closedBall_scale line 56
5. def OAI.CAT0Fillings.JointBV.LocalMeanBound line 61
6. lemma OAI.CAT0Fillings.JointBV.average_half_bound line 66
7. lemma OAI.CAT0Fillings.JointBV.point_average_bound line 88
8. lemma OAI.CAT0Fillings.JointBV.average_neighbor_bound line 120
9. lemma OAI.CAT0Fillings.JointBV.ae_ballAverage_tendsto line 143
10. lemma OAI.CAT0Fillings.JointBV.dyadic_closedBall_average_tendsto line 150
11. lemma OAI.CAT0Fillings.JointBV.abs_sub_le_of_localMeanBound line 163
12. lemma OAI.CAT0Fillings.JointBV.integral_abs_le_of_ae_tendsto line 200
13. lemma OAI.CAT0Fillings.JointBV.pair_integral_le_oscillation line 220
14. lemma OAI.CAT0Fillings.JointBV.oscillation_le_pair_integral line 234
15. theorem OAI.CAT0Fillings.JointBV.ball_poincare_of_smooth_approx line 250