OAI/Probability/ProjectionMoments/WeightedCover.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ProjectionMoments.Weighted.budget line 16
2. lemma OAI.ProjectionMoments.Weighted.budget_closed line 19
3. lemma OAI.ProjectionMoments.Weighted.budget_mem_single line 26
4. lemma OAI.ProjectionMoments.Weighted.budget_compact line 31
5. lemma OAI.ProjectionMoments.Weighted.budget_convex line 37
6. lemma OAI.ProjectionMoments.Weighted.cost_summable line 53
7. lemma OAI.ProjectionMoments.Weighted.cost_le line 57
8. lemma OAI.ProjectionMoments.Weighted.eval_summable line 61
9. lemma OAI.ProjectionMoments.Weighted.eval_le line 67
10. lemma OAI.ProjectionMoments.Weighted.eval_tail line 73
11. lemma OAI.ProjectionMoments.Weighted.eval_continuousOn line 104
12. lemma OAI.ProjectionMoments.Weighted.zero_mem_budget line 132
13. lemma OAI.ProjectionMoments.Weighted.single_mem_budget line 137
14. lemma OAI.ProjectionMoments.Weighted.eval_single line 159
15. lemma OAI.ProjectionMoments.Weighted.eval_smul_add line 165
16. lemma OAI.ProjectionMoments.Weighted.finite_dual_domination line 174
17. theorem OAI.ProjectionMoments.Weighted.dual_domination line 262
18. lemma OAI.ProjectionMoments.Weighted.lintegral_finite_test line 291
19. theorem OAI.ProjectionMoments.Weighted.measure_domination line 304
20. theorem OAI.ProjectionMoments.Weighted.measure_domination_nonneg line 362