OAI/Analysis/C0Absorption/Shift.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.C0Absorption.frozenShift line 14
  2. theorem OAI.C0Absorption.frozenShift_apply line 16
  3. theorem OAI.C0Absorption.frozenShift_bound line 19
  4. def OAI.C0Absorption.blockInclusion line 25
  5. theorem OAI.C0Absorption.blockInclusion_apply line 28
  6. def OAI.C0Absorption.outputScalar line 31
  7. theorem OAI.C0Absorption.outputScalar_apply line 34
  8. theorem OAI.C0Absorption.outputScalar_bound line 38
  9. theorem OAI.C0Absorption.outputScalar_tendsto line 44
  10. def OAI.C0Absorption.firstLevel line 49
  11. theorem OAI.C0Absorption.firstLevel_injective line 51
  12. theorem OAI.C0Absorption.levelSuccessor_injective line 53
  13. def OAI.C0Absorption.inverseRows line 58
  14. def OAI.C0Absorption.inverseBlockFunction line 62
  15. theorem OAI.C0Absorption.inverseBlockFunction_tendsto line 65
  16. def OAI.C0Absorption.inverseBlocks line 84
  17. def OAI.C0Absorption.frozenInverse line 87
  18. theorem OAI.C0Absorption.frozenInverse_row line 89
  19. theorem OAI.C0Absorption.frozenInverse_block line 92
  20. theorem OAI.C0Absorption.frozenInverse_bound line 95
  21. def OAI.C0Absorption.frozenInverseL line 117
  22. theorem OAI.C0Absorption.finite_row_cancel line 146
  23. theorem OAI.C0Absorption.finite_row_shift line 150
  24. theorem OAI.C0Absorption.rowScalar_frozenInverse line 154
  25. theorem OAI.C0Absorption.previousScalar_frozenInverse line 164
  26. theorem OAI.C0Absorption.frozenShift_frozenInverse line 171
  27. theorem OAI.C0Absorption.outputScalar_frozenShift line 177
  28. theorem OAI.C0Absorption.frozenInverse_frozenShift line 186
  29. def OAI.C0Absorption.frozenEquiv line 204
  30. theorem OAI.C0Absorption.frozenShift_lower line 214
  31. def OAI.C0Absorption.recomputedShift line 225
  32. theorem OAI.C0Absorption.recomputedShift_zero line 227
  33. theorem OAI.C0Absorption.WeightError.smul line 229
  34. theorem OAI.C0Absorption.WeightError.mono line 241
  35. theorem OAI.C0Absorption.normalized_error_left line 244
  36. theorem OAI.C0Absorption.normalized_error_right line 254
  37. theorem OAI.C0Absorption.shift_weight_error line 264
  38. theorem OAI.C0Absorption.recomputed_mixed_left line 272
  39. theorem OAI.C0Absorption.recomputed_mixed_right line 277
  40. theorem OAI.C0Absorption.recomputed_mixed_approx line 282
  41. theorem OAI.C0Absorption.recomputed_global_bounds line 290
  42. theorem OAI.C0Absorption.recomputed_lipschitz line 305
  43. theorem OAI.C0Absorption.recomputed_antilipschitz line 312