OAI/Analysis/C0Absorption/FiniteShift.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.C0Absorption.finiteRecomputed line 16
  2. theorem OAI.C0Absorption.finiteRecomputed_zero line 19
  3. theorem OAI.C0Absorption.finiteFrozen_weight_error line 21
  4. theorem OAI.C0Absorption.finiteRecomputed_mixed_left line 34
  5. theorem OAI.C0Absorption.finiteRecomputed_mixed_right line 41
  6. theorem OAI.C0Absorption.finiteRecomputed_mixed_approx line 48
  7. theorem OAI.C0Absorption.fiveBounds_of_error line 57
  8. theorem OAI.C0Absorption.finiteRecomputed_global_bounds line 64
  9. theorem OAI.C0Absorption.finiteRecomputed_lipschitz line 79
  10. theorem OAI.C0Absorption.finiteRecomputed_antilipschitz line 86
  11. theorem OAI.C0Absorption.finite_operator_norm_le_columns line 104
  12. theorem OAI.C0Absorption.tendsto_finiteOperator_of_columns line 122
  13. theorem OAI.C0Absorption.diagonal_neighborhood line 135