OAI/Analysis/C0Absorption/Correction.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.C0Absorption.blockVector line 14
  2. def OAI.C0Absorption.blockRow line 17
  3. theorem OAI.C0Absorption.blockVector_nonneg line 20
  4. theorem OAI.C0Absorption.blockVector_le_one line 23
  5. theorem OAI.C0Absorption.blockRow_nonneg line 29
  6. theorem OAI.C0Absorption.blockRow_sum line 32
  7. theorem OAI.C0Absorption.blockRow_vector line 39
  8. theorem OAI.C0Absorption.bandL_ge_dyadic_inv line 59
  9. theorem OAI.C0Absorption.bandVector_distance line 65
  10. theorem OAI.C0Absorption.theta_band_budget line 70
  11. theorem OAI.C0Absorption.bandRow_scaled_difference line 91
  12. theorem OAI.C0Absorption.blockRow_distance_decompose line 103
  13. theorem OAI.C0Absorption.blockRow_weighted_distance line 118
  14. theorem OAI.C0Absorption.product_difference_bound line 165
  15. theorem OAI.C0Absorption.theta_weighted_coordinate line 174
  16. theorem OAI.C0Absorption.blockVector_weighted_distance line 180
  17. theorem OAI.C0Absorption.bandRow_continuous line 218
  18. theorem OAI.C0Absorption.localRadius_continuous line 222
  19. theorem OAI.C0Absorption.blockVector_continuous line 225
  20. theorem OAI.C0Absorption.blockRow_continuous line 229