OAI/Analysis/SegmentLenses/Averaged.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SegmentLenses.finite_head_average line 21
2. theorem OAI.SegmentLenses.predual_unit_approx line 59
3. theorem OAI.SegmentLenses.predual_averaged_witness line 95
4. theorem OAI.SegmentLenses.coordinate_independent line 122
5. theorem OAI.SegmentLenses.predualCoordinate_independent line 129
6. theorem OAI.SegmentLenses.predual_not_finite line 132
7. theorem OAI.SegmentLenses.fullDual_not_finite line 138
8. instance OAI.SegmentLenses.(instance at line 146) line 146
9. structure OAI.SegmentLenses.CofiniteSubspace line 158
10. abbrev OAI.SegmentLenses.SphereOne line 165
11. abbrev OAI.SegmentLenses.CofiniteSphere line 166
12. def OAI.SegmentLenses.CofiniteSubspace.ofMap line 170
13. instance OAI.SegmentLenses.(instance at line 177) line 177
14. theorem OAI.SegmentLenses.CofiniteSubspace.sphere_nonempty line 180
15. theorem OAI.SegmentLenses.sphereOne_nonempty line 193
16. def OAI.SegmentLenses.averagedOn line 198
17. def OAI.SegmentLenses.averagedAt line 201
18. def OAI.SegmentLenses.averagedModulus line 205
19. theorem OAI.SegmentLenses.average_bounds line 208
20. theorem OAI.SegmentLenses.averagedOn_bounds line 221
21. theorem OAI.SegmentLenses.averagedAt_bdd line 235
22. theorem OAI.SegmentLenses.averagedModulus_lower line 244
23. def OAI.SegmentLenses.predualHeadValues line 267
24. theorem OAI.SegmentLenses.predualHeadValues_zero line 271
25. theorem OAI.SegmentLenses.predual_all_radius_average line 286
26. theorem OAI.SegmentLenses.infinite_all_radius_average line 296