OAI/Analysis/LipschitzEquivalence/CompactLocalization.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.LipschitzCounterexample.LocalizedLinearization.cutoff_nonzero_mem line 20
  2. theorem OAI.LipschitzCounterexample.LocalizedLinearization.disjoint_cutoffs line 27
  3. theorem OAI.LipschitzCounterexample.LocalizedLinearization.sum_cutoff_bounds line 34
  4. def OAI.LipschitzCounterexample.LocalizedLinearization.removed line 53
  5. def OAI.LipschitzCounterexample.LocalizedLinearization.remainder line 56
  6. theorem OAI.LipschitzCounterexample.LocalizedLinearization.removed_lipschitz line 59
  7. theorem OAI.LipschitzCounterexample.LocalizedLinearization.remainder_lipschitz line 75
  8. theorem OAI.LipschitzCounterexample.LocalizedLinearization.remainder_inner line 84
  9. theorem OAI.LipschitzCounterexample.LocalizedLinearization.remainder_tendsto_zero line 103
  10. theorem OAI.LipschitzCounterexample.LocalizedLinearization.remainder_compact_lipschitz line 110
  11. theorem OAI.LipschitzCounterexample.LocalizedLinearization.test_normalized_sum line 164
  12. theorem OAI.LipschitzCounterexample.LocalizedLinearization.removed_pairings_small line 187
  13. theorem OAI.LipschitzCounterexample.LocalizedLinearization.scalar_localization line 235