OAI/Analysis/AncientFlat/Geometry/ExtensionGeometry.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.FlatWeighted.sigma_sq line 11
2. lemma OAI.FlatWeighted.norm_le_sigma line 14
3. lemma OAI.FlatWeighted.pdist_symm line 19
4. lemma OAI.FlatWeighted.sigma_le_add_pdist line 22
5. def OAI.FlatWeighted.timeProject line 52
6. def OAI.FlatWeighted.extensionWeight line 53
7. lemma OAI.FlatWeighted.innerExtension_eq line 55
8. lemma OAI.FlatWeighted.timeProject_mem line 61
9. lemma OAI.FlatWeighted.timeProject_pdist line 65
10. lemma OAI.FlatWeighted.sigma_project_le line 70
11. lemma OAI.FlatWeighted.extensionWeight_range line 74
12. lemma OAI.FlatWeighted.sigma_le_project_of_active line 84