OAI/Analysis/LipschitzEquivalence/SmoothMultiplier.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LipschitzCounterexample.CompactWSC.abs_prod_le_one line 13
2. theorem OAI.LipschitzCounterexample.CompactWSC.abs_prod_sub_prod_le line 18
3. def OAI.LipschitzCounterexample.CompactWSC.damping line 42
4. theorem OAI.LipschitzCounterexample.CompactWSC.damping_nonneg line 45
5. theorem OAI.LipschitzCounterexample.CompactWSC.damping_le_one line 53
6. theorem OAI.LipschitzCounterexample.CompactWSC.one_sub_damping_le line 63
7. theorem OAI.LipschitzCounterexample.CompactWSC.exists_smooth_multiplier line 74
8. theorem OAI.LipschitzCounterexample.CompactWSC.product_gradient_error line 115