OAI/Analysis/LipschitzEquivalence/CauchyReduction.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.LipschitzCounterexample.FreeSpace.CauchyLocalizationState line 20
2. theorem OAI.LipschitzCounterexample.FreeSpace.cauchy_localization_step line 29
3. theorem OAI.LipschitzCounterexample.FreeSpace.bounded_cauchy_compact_reduction line 60
4. theorem OAI.LipschitzCounterexample.FreeSpace.cauchy_compact_reduction line 130
5. theorem OAI.LipschitzCounterexample.WeakSequences.weakCauchy_biddual_limit line 151
6. theorem OAI.LipschitzCounterexample.WeakSequences.wsc_of_uniform_weak_approx line 168
7. theorem OAI.LipschitzCounterexample.FreeSpace.wsc_of_compact_supported line 206