OAI/Analysis/LipschitzHilbert/Phase/AngularErrorFamily.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Actual dyadic angular-error coefficients and their constructed line majorant. The assumptions are packet and multiplier bounds, not an error concentration or convolution estimate.

  1. structure OAI.LipschitzHilbert.AngularErrorFamily line 17
  2. def OAI.LipschitzHilbert.AngularErrorFamily.length line 68
  3. def OAI.LipschitzHilbert.AngularErrorFamily.angleStep line 69
  4. def OAI.LipschitzHilbert.AngularErrorFamily.coefficient line 71
  5. def OAI.LipschitzHilbert.AngularErrorFamily.scaleError line 75
  6. def OAI.LipschitzHilbert.AngularErrorFamily.error line 80
  7. def OAI.LipschitzHilbert.AngularErrorFamily.sourceAmplitude line 82
  8. theorem OAI.LipschitzHilbert.AngularErrorFamily.sourceAmplitude_nonneg line 85
  9. def OAI.LipschitzHilbert.AngularErrorFamily.sources line 92
  10. theorem OAI.LipschitzHilbert.AngularErrorFamily.scaleError_le line 97
  11. theorem OAI.LipschitzHilbert.AngularErrorFamily.error_le_majorant line 119