OAI/Analysis/C0Absorption/Grid.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.C0Absorption.BandGrid line 14
  2. abbrev OAI.C0Absorption.PrefixCube line 15
  3. def OAI.C0Absorption.bandPoint line 17
  4. def OAI.C0Absorption.prefixRestrict line 20
  5. theorem OAI.C0Absorption.prefixRestrict_lipschitz line 25
  6. def OAI.C0Absorption.bandBump line 33
  7. def OAI.C0Absorption.bandVector line 36
  8. def OAI.C0Absorption.bandDenominator line 39
  9. def OAI.C0Absorption.bandRow line 41
  10. theorem OAI.C0Absorption.bandBump_nonneg line 44
  11. theorem OAI.C0Absorption.bandVector_nonneg line 47
  12. theorem OAI.C0Absorption.bandVector_le_one line 50
  13. theorem OAI.C0Absorption.bandVector_eq_one line 53
  14. theorem OAI.C0Absorption.bandVector_support line 62
  15. theorem OAI.C0Absorption.const_dist_div_lipschitz line 72
  16. theorem OAI.C0Absorption.bandBump_lipschitz line 81
  17. theorem OAI.C0Absorption.bandVector_lipschitz line 85
  18. theorem OAI.C0Absorption.bandDenominator_ge line 89
  19. theorem OAI.C0Absorption.bandDenominator_pos line 107
  20. theorem OAI.C0Absorption.bandRow_nonneg line 110
  21. theorem OAI.C0Absorption.bandRow_sum line 113
  22. theorem OAI.C0Absorption.bandRow_vector line 118
  23. theorem OAI.C0Absorption.normalized_sum_distance line 127
  24. def OAI.C0Absorption.bandL line 162
  25. theorem OAI.C0Absorption.bandRow_distance line 164