OAI/Analysis/LipschitzHilbert/Estimates/ActualErrorSource.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The manuscript's annular error indicator and small-angle ratio, including its logarithmic dyadic-branching source-sum bound.

  1. def OAI.LipschitzHilbert.errorSourceProfile line 17
  2. theorem OAI.LipschitzHilbert.errorSourceProfile_measurable line 20
  3. theorem OAI.LipschitzHilbert.errorSourceProfile_le_dyadic line 29
  4. theorem OAI.LipschitzHilbert.errorSourceProfile_nonneg line 42
  5. theorem OAI.LipschitzHilbert.errorSourceProfile_bound line 47
  6. theorem OAI.LipschitzHilbert.sum_errorSourceProfile line 57
  7. theorem OAI.LipschitzHilbert.sum_errorSourceProfile_branching line 63