OAI/Analysis/LipschitzHilbert/Trees/FourGridBandErrors.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Actual radix-four meshes and the geometric error bound for each band.

  1. def OAI.LipschitzHilbert.fourGrid line 15
  2. theorem OAI.LipschitzHilbert.fourGrid_mesh line 23
  3. def OAI.LipschitzHilbert.bandInner line 27
  4. def OAI.LipschitzHilbert.bandOuter line 28
  5. theorem OAI.LipschitzHilbert.bandInner_pos line 30
  6. theorem OAI.LipschitzHilbert.bandInner_scale line 32
  7. theorem OAI.LipschitzHilbert.bandOuter_scale line 36
  8. theorem OAI.LipschitzHilbert.four_pow_ratio line 40
  9. def OAI.LipschitzHilbert.bandErrorAt line 47
  10. def OAI.LipschitzHilbert.bandError line 50
  11. theorem OAI.LipschitzHilbert.geometric_band_error line 53
  12. theorem OAI.LipschitzHilbert.fourGrid_band_error line 104