OAI/Analysis/LipschitzEquivalence/WUCFunctions.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LipschitzCounterexample.CompactWSC.halfWeight line 13
2. theorem OAI.LipschitzCounterexample.CompactWSC.halfWeight_pos line 15
3. theorem OAI.LipschitzCounterexample.CompactWSC.sum_halfWeight line 17
4. theorem OAI.LipschitzCounterexample.CompactWSC.sum_halfWeight_le line 22
5. theorem OAI.LipschitzCounterexample.CompactWSC.halfWeight_le_one line 26
6. theorem OAI.LipschitzCounterexample.CompactWSC.damping_telescope line 30
7. theorem OAI.LipschitzCounterexample.CompactWSC.sum_grad_norm_le line 42
8. theorem OAI.LipschitzCounterexample.CompactWSC.signed_sum_lipschitz line 62
9. theorem OAI.LipschitzCounterexample.CompactWSC.exists_wuc_functions line 89