OAI/Analysis/AncientFlat/Geometry/AnnularCompactHolder.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ParabolicAnnular.rectangle line 9
2. lemma OAI.ParabolicAnnular.rectangle_compact line 10
3. lemma OAI.ParabolicAnnular.rectangle_convex line 11
4. lemma OAI.ParabolicAnnular.outer_to_rectangle line 13
5. lemma OAI.ParabolicAnnular.norm_radial_pair_le line 16
6. lemma OAI.ParabolicAnnular.compact_radial_holder line 31