OAI/Analysis/LipschitzHilbert/Estimates/PositiveErrorMajorant.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

The actual positive convolution majorant for the error terms. Source size and source-sum bounds remain explicit; BMO is derived for this majorant rather than assumed for every function it dominates.

  1. structure OAI.LipschitzHilbert.LineErrorSources line 18
  2. def OAI.LipschitzHilbert.LineErrorSources.length line 37
  3. def OAI.LipschitzHilbert.LineErrorSources.term line 38
  4. def OAI.LipschitzHilbert.LineErrorSources.majorant line 39
  5. def OAI.LipschitzHilbert.LineErrorSources.shortPart line 40
  6. def OAI.LipschitzHilbert.LineErrorSources.longPart line 41
  7. def OAI.LipschitzHilbert.LineErrorSources.meanConstant line 42
  8. def OAI.LipschitzHilbert.LineErrorSources.oscillationConstant line 43
  9. theorem OAI.LipschitzHilbert.LineErrorSources.length_pos line 45
  10. theorem OAI.LipschitzHilbert.LineErrorSources.source_norm_bound line 48
  11. theorem OAI.LipschitzHilbert.LineErrorSources.term_nonneg line 53
  12. theorem OAI.LipschitzHilbert.LineErrorSources.term_continuous line 56
  13. theorem OAI.LipschitzHilbert.LineErrorSources.majorant_nonneg line 59
  14. theorem OAI.LipschitzHilbert.LineErrorSources.majorant_continuous line 62
  15. theorem OAI.LipschitzHilbert.LineErrorSources.shortPart_nonneg line 65
  16. theorem OAI.LipschitzHilbert.LineErrorSources.shortPart_continuous line 68
  17. theorem OAI.LipschitzHilbert.LineErrorSources.longPart_continuous line 76
  18. theorem OAI.LipschitzHilbert.LineErrorSources.majorant_split line 84
  19. theorem OAI.LipschitzHilbert.LineErrorSources.shortPart_integral line 94
  20. theorem OAI.LipschitzHilbert.LineErrorSources.longPart_oscillation line 99
  21. theorem OAI.LipschitzHilbert.LineErrorSources.majorant_mean_oscillation line 105