OAI/Probability/SignedSweeps/HullDensityComparison.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SignedSweeps.isClosed_quadratic_upper line 13
2. lemma OAI.SignedSweeps.convex_quadratic_upper line 19
3. lemma OAI.SignedSweeps.quadratic_upper_closed_convex line 31
4. lemma OAI.SignedSweeps.projection_norm_sq_le_of_hull_domination line 41
5. lemma OAI.SignedSweeps.right_projection_norm_sq_le_of_hull_domination line 72
6. theorem OAI.SignedSweeps.one_sided_hull_density_comparison line 90