OAI/Analysis/C0Absorption/Operators.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.C0Absorption.cfunOfTendsto line 18
  2. theorem OAI.C0Absorption.cfun_tendsto line 23
  3. theorem OAI.C0Absorption.cfun_norm_apply_le line 26
  4. theorem OAI.C0Absorption.cfun_norm_le line 29
  5. def OAI.C0Absorption.cfunPull line 33
  6. theorem OAI.C0Absorption.cfunPull_apply line 36
  7. def OAI.C0Absorption.cfunPullL line 39
  8. theorem OAI.C0Absorption.cfunPullL_apply line 48
  9. theorem OAI.C0Absorption.tendsto_sumElim_cofinite line 53
  10. abbrev OAI.C0Absorption.BlockC0 line 65
  11. def OAI.C0Absorption.inputRows line 67
  12. def OAI.C0Absorption.inputBlocks line 69
  13. theorem OAI.C0Absorption.inputRows_apply line 71
  14. theorem OAI.C0Absorption.inputBlocks_apply line 72
  15. def OAI.C0Absorption.joinInputs line 74
  16. theorem OAI.C0Absorption.joinInputs_row line 79
  17. theorem OAI.C0Absorption.joinInputs_block line 84
  18. theorem OAI.C0Absorption.joinInputs_split line 89
  19. theorem OAI.C0Absorption.joinInputs_norm line 96
  20. def OAI.C0Absorption.inputCoordinates line 115
  21. theorem OAI.C0Absorption.labelLevel_tendsto line 140
  22. theorem OAI.C0Absorption.labelRadius_tendsto line 143
  23. theorem OAI.C0Absorption.frozenCorrection_tendsto line 146
  24. def OAI.C0Absorption.frozenCorrectionC0 line 151
  25. def OAI.C0Absorption.frozenCorrectionL line 154
  26. theorem OAI.C0Absorption.frozenCorrectionL_apply line 163
  27. def OAI.C0Absorption.correctionC0 line 166
  28. theorem OAI.C0Absorption.correctionC0_apply line 168