OAI/Analysis/LipschitzHilbert/Trees/SourceLineGrid.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The actual nested line grid with the rounded manuscript step. A single refinement has mesh H/G, small enough to retain the G^(-1/16) error when the carrier spread times H is at most G^(15/16).

  1. def OAI.LipschitzHilbert.sourceLineGrid line 13
  2. theorem OAI.LipschitzHilbert.sourceLineGrid_mesh line 21
  3. theorem OAI.LipschitzHilbert.sourceLineGrid_mesh_carrier line 26
  4. theorem OAI.LipschitzHilbert.source_prediction_error_le line 39