OAI/Geometry/CAT0Fillings/Reconstruction/ScalarKernel.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CAT0Fillings.SliceReconstruction.realCone line 15
2. lemma OAI.CAT0Fillings.SliceReconstruction.realCone_lipschitz line 18
3. def OAI.CAT0Fillings.SliceReconstruction.coneApprox line 27
4. lemma OAI.CAT0Fillings.SliceReconstruction.coneApprox_lipschitz line 31
5. lemma OAI.CAT0Fillings.SliceReconstruction.le_coneApprox line 37
6. lemma OAI.CAT0Fillings.SliceReconstruction.coneApprox_antitone line 43
7. lemma OAI.CAT0Fillings.SliceReconstruction.coneApprox_le_cone line 47
8. lemma OAI.CAT0Fillings.SliceReconstruction.coneApprox_tendsto line 54
9. lemma OAI.CAT0Fillings.SliceReconstruction.scalar_update line 84
10. def OAI.CAT0Fillings.SliceReconstruction.ScalarKernel line 94
11. lemma OAI.CAT0Fillings.SliceReconstruction.ScalarKernel.const line 97
12. lemma OAI.CAT0Fillings.SliceReconstruction.ScalarKernel.linear line 102
13. lemma OAI.CAT0Fillings.SliceReconstruction.ScalarKernel.min line 111
14. lemma OAI.CAT0Fillings.SliceReconstruction.ScalarKernel.neg line 146
15. lemma OAI.CAT0Fillings.SliceReconstruction.ScalarKernel.max line 151
16. lemma OAI.CAT0Fillings.SliceReconstruction.ScalarKernel.limit line 167
17. lemma OAI.CAT0Fillings.SliceReconstruction.ScalarKernel.cone line 177
18. lemma OAI.CAT0Fillings.SliceReconstruction.ScalarKernel.comp line 202
19. lemma OAI.CAT0Fillings.SliceReconstruction.ScalarKernel.of_boundedLip line 216
20. theorem OAI.CAT0Fillings.SliceReconstruction.current_eq_zero_on_scalar_graph line 229
21. theorem OAI.CAT0Fillings.SliceReconstruction.current_eq_on_scalar_graph line 275