OAI/Analysis/LipschitzEquivalence/BlockSelection.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LipschitzCounterexample.CompactWSC.half_sum_lipschitz line 14
2. theorem OAI.LipschitzCounterexample.CompactWSC.half_sub_lipschitz line 27
3. theorem OAI.LipschitzCounterexample.CompactWSC.dyadicMean_lipschitz line 31
4. theorem OAI.LipschitzCounterexample.CompactWSC.dyadicMean_zero_value line 41
5. def OAI.LipschitzCounterexample.CompactWSC.halfBlock line 50
6. theorem OAI.LipschitzCounterexample.CompactWSC.halfBlock_lipschitz line 53
7. theorem OAI.LipschitzCounterexample.CompactWSC.halfBlock_zero_value line 60
8. theorem OAI.LipschitzCounterexample.CompactWSC.augmentedEnergy_smul line 65
9. theorem OAI.LipschitzCounterexample.CompactWSC.one_augmentedEnergy_le line 74
10. theorem OAI.LipschitzCounterexample.CompactWSC.select_block line 86