OAI/Geometry/QuadricBundles/BallAverage.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.QuadricCounterexample.continuous_ball_integral line 19
2. theorem OAI.QuadricCounterexample.continuous_ball_average line 53
3. lemma OAI.QuadricCounterexample.ball_average_nonneg line 67
4. lemma OAI.QuadricCounterexample.ball_average_le_const line 74
5. theorem OAI.QuadricCounterexample.ball_infimum_representative_limit line 88
6. lemma OAI.QuadricCounterexample.ball_average_eq_closedBall_average line 124
7. theorem OAI.QuadricCounterexample.ball_infimum_representative_ae line 131