OAI/Analysis/LipschitzEquivalence/FiniteMultipliers.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LipschitzCounterexample.FreeSpace.maps_agree_of_points line 20
2. theorem OAI.LipschitzCounterexample.FreeSpace.norm_sub_apply_le_of_agree line 31
3. def OAI.LipschitzCounterexample.FreeSpace.outerRadius line 40
4. theorem OAI.LipschitzCounterexample.FreeSpace.outerRadius_pos line 42
5. def OAI.LipschitzCounterexample.FreeSpace.radialMultiplier line 44
6. theorem OAI.LipschitzCounterexample.FreeSpace.cutoff_abs_le_one line 47
7. theorem OAI.LipschitzCounterexample.FreeSpace.cutoff_radius_bound line 51
8. theorem OAI.LipschitzCounterexample.FreeSpace.radialMultiplier_point line 56
9. theorem OAI.LipschitzCounterexample.FreeSpace.norm_radialMultiplier_le line 60
10. theorem OAI.LipschitzCounterexample.FreeSpace.radialMultiplier_identity line 69
11. theorem OAI.LipschitzCounterexample.FreeSpace.radialMultiplier_supported line 78
12. theorem OAI.LipschitzCounterexample.FreeSpace.bounded_weak_approx line 85
13. def OAI.LipschitzCounterexample.FreeSpace.finiteCutoff line 104
14. def OAI.LipschitzCounterexample.FreeSpace.finiteCutoffLip line 107
15. def OAI.LipschitzCounterexample.FreeSpace.finiteMultiplier line 109
16. theorem OAI.LipschitzCounterexample.FreeSpace.finiteCutoff_lipschitz line 112
17. theorem OAI.LipschitzCounterexample.FreeSpace.finiteCutoff_abs_le_one line 122
18. theorem OAI.LipschitzCounterexample.FreeSpace.finiteCutoff_radius_bound line 129
19. theorem OAI.LipschitzCounterexample.FreeSpace.finiteMultiplier_point line 133
20. def OAI.LipschitzCounterexample.FreeSpace.finiteMultiplierBound line 138
21. theorem OAI.LipschitzCounterexample.FreeSpace.norm_finiteMultiplier_le line 140
22. theorem OAI.LipschitzCounterexample.FreeSpace.finiteMultiplier_agree line 145
23. theorem OAI.LipschitzCounterexample.FreeSpace.finiteMultiplier_support line 157
24. theorem OAI.LipschitzCounterexample.FreeSpace.finiteMultiplier_error line 170