OAI/Analysis/LipschitzEquivalence/SlotBudget.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LipschitzCounterexample.HilbertSlots.velocity_budget line 14
2. def OAI.LipschitzCounterexample.HilbertSlots.ofSqBound line 30
3. theorem OAI.LipschitzCounterexample.HilbertSlots.ofSqBound_apply line 37
4. theorem OAI.LipschitzCounterexample.HilbertSlots.norm_ofSqBound_sq_le line 41
5. theorem OAI.LipschitzCounterexample.HilbertSlots.interleave_coordinate_sq line 48
6. theorem OAI.LipschitzCounterexample.HilbertSlots.residual_coefficient_sq line 68
7. theorem OAI.LipschitzCounterexample.HilbertSlots.first_error_sq line 80
8. theorem OAI.LipschitzCounterexample.HilbertSlots.inner_error_sq line 87
9. def OAI.LipschitzCounterexample.HilbertSlots.slotError line 97
10. theorem OAI.LipschitzCounterexample.HilbertSlots.norm_slotError line 106