OAI/Analysis/LipschitzHilbert/Estimates/ErrorSourceBridge.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Construction of the line error data from the manuscript's actual two-coordinate direction profile and common vertical averaging kernel.

  1. def OAI.LipschitzHilbert.actualErrorSources line 16
  2. theorem OAI.LipschitzHilbert.actualErrorSources_source line 45
  3. theorem OAI.LipschitzHilbert.actualErrorSources_log_sumBound line 53
  4. theorem OAI.LipschitzHilbert.source_branching_eq_two_pow line 65