OAI/Analysis/C0Absorption/Selection.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.C0Absorption.thin_sequence line 13
  2. theorem OAI.C0Absorption.finite_constant_subsequence line 21
  3. theorem OAI.C0Absorption.constant_or_injective_subsequence line 33
  4. theorem OAI.C0Absorption.nat_constant_or_tendsto line 49
  5. theorem OAI.C0Absorption.finite_subsequence_selection line 66
  6. theorem OAI.C0Absorption.choose_mono_sequence line 87
  7. theorem OAI.C0Absorption.nested_selection_lipschitz line 108
  8. structure OAI.C0Absorption.TagLocalization line 153
  9. theorem OAI.C0Absorption.TagLocalization.representation_support line 163
  10. theorem OAI.C0Absorption.TagLocalization.projected_concentration line 173
  11. theorem OAI.C0Absorption.high_bands_compatible line 211