OAI/Analysis/C0Absorption/Pairings.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.C0Absorption.completedPairing line 16
  2. def OAI.C0Absorption.initialPairing line 19
  3. theorem OAI.C0Absorption.initialPairing_lipschitz line 24
  4. theorem OAI.C0Absorption.completedPairing_coe line 34
  5. theorem OAI.C0Absorption.completedPairing_lipschitz line 39
  6. def OAI.C0Absorption.completedTest line 44
  7. theorem OAI.C0Absorption.completedTest_eq line 48
  8. def OAI.C0Absorption.AdmissibleList.singleton line 60
  9. theorem OAI.C0Absorption.singleton_norm line 71
  10. theorem OAI.C0Absorption.test_pairing_bound line 81
  11. theorem OAI.C0Absorption.list_test_pairing_bound line 91
  12. theorem OAI.C0Absorption.completedList_apply line 98
  13. theorem OAI.C0Absorption.pairing_tendsto line 112
  14. theorem OAI.C0Absorption.completedPairing_tendsto line 121
  15. def OAI.C0Absorption.transferredList line 145
  16. theorem OAI.C0Absorption.listExponent_toReal_pos line 154
  17. theorem OAI.C0Absorption.exists_smaller_exponent line 158
  18. theorem OAI.C0Absorption.fixed_sigma_detector line 169
  19. theorem OAI.C0Absorption.nonnegative_has_positive_subsequence line 214
  20. theorem OAI.C0Absorption.bounded_signs_norm_each line 225
  21. theorem OAI.C0Absorption.bounded_signs_weak_null line 239
  22. theorem OAI.C0Absorption.completedCoordinate_eq_weight_sigma line 267
  23. theorem OAI.C0Absorption.one_class_detects line 273