OAI/Analysis/C0Absorption/Lists.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.C0Absorption.completedSigma line 16
  2. theorem OAI.C0Absorption.completedSigma_coe line 19
  3. theorem OAI.C0Absorption.completedSigma_continuous line 28
  4. theorem OAI.C0Absorption.sigma_le_preNorm line 31
  5. theorem OAI.C0Absorption.completedSigma_le line 41
  6. def OAI.C0Absorption.initialList line 51
  7. def OAI.C0Absorption.completedList line 57
  8. theorem OAI.C0Absorption.completedList_coe line 61
  9. theorem OAI.C0Absorption.completedList_le_sigma line 67
  10. def OAI.C0Absorption.completedListNorm line 80
  11. theorem OAI.C0Absorption.completedListNorm_bddAbove line 84
  12. def OAI.C0Absorption.sigmaFromLists line 90
  13. theorem OAI.C0Absorption.sigmaFromLists_le line 93
  14. theorem OAI.C0Absorption.sigmaFromLists_eq line 99
  15. theorem OAI.C0Absorption.completedSigma_eq_iSup line 115
  16. theorem OAI.C0Absorption.finite_lp_norm_rpow line 126
  17. theorem OAI.C0Absorption.finite_lp_interpolation line 134
  18. theorem OAI.C0Absorption.exists_uniform_lp_detector line 152
  19. theorem OAI.C0Absorption.tendsto_of_dense_lipschitz line 181