OAI/Geometry/CylinderCovering/Convexity/FiniteCauchyVariation.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ProjectionConcavity.abs_add_abs_sub_of_abs_le line 11
2. lemma OAI.ProjectionConcavity.exists_pos_mul_abs_le line 26
3. lemma OAI.ProjectionConcavity.normalize_decreases line 53
4. theorem OAI.ProjectionConcavity.exists_unit_lower_abs_inner_sum line 70
5. lemma OAI.ProjectionConcavity.exists_unit_orthogonal_of_finrank_lt line 107
6. theorem OAI.ProjectionConcavity.minimizing_unit_annihilates_two line 124
7. theorem OAI.ProjectionConcavity.exists_minimizing_unit_annihilates_two line 171