OAI/Probability/ProjectionMoments/CapTests.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ProjectionMoments.cap_mass_inv_bound line 13
2. lemma OAI.ProjectionMoments.cap_ratio_algebra line 32
3. lemma OAI.ProjectionMoments.cap_cost_ratio line 51
4. lemma OAI.ProjectionMoments.cap_small_scale_constant line 65
5. lemma OAI.ProjectionMoments.weighted_cap_set_le line 80
6. def OAI.ProjectionMoments.capTestMeasure line 89
7. lemma OAI.ProjectionMoments.capTestMeasure_mass line 92
8. lemma OAI.ProjectionMoments.capTestMeasure_finite line 101
9. lemma OAI.ProjectionMoments.capTestMeasure_support line 107
10. lemma OAI.ProjectionMoments.capTestMeasure_ball line 117
11. lemma OAI.ProjectionMoments.capTest_allBall line 127
12. lemma OAI.ProjectionMoments.rescaled_projection_ac line 183
13. lemma OAI.ProjectionMoments.capTest_frame_ac line 203