OAI/Analysis/AncientFlat/Geometry/WindowGeometry.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ParabolicLocalization.windowInv line 9
2. lemma OAI.ParabolicLocalization.window_windowInv line 12
3. lemma OAI.ParabolicLocalization.window_zero line 18
4. lemma OAI.ParabolicLocalization.pow_quarter_four line 20
5. lemma OAI.ParabolicLocalization.cylinder_pdist_zero line 24
6. lemma OAI.ParabolicLocalization.small_window_maps line 32
7. lemma OAI.ParabolicLocalization.windowInv_mem_one line 54
8. lemma OAI.ParabolicLocalization.close_pair_window line 69