OAI/Analysis/LipschitzHilbert/Geometry/LineConvolutionFar.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

First kernel moments control the contribution of bounded data outside an enlarged interval. This is the far part of the smooth Carleson measure.

  1. theorem OAI.LipschitzHilbert.PacketRepresentation.lineConvolution_bound_of_gap line 12
  2. theorem OAI.LipschitzHilbert.PacketRepresentation.lineProjection_far_bound line 33
  3. theorem OAI.LipschitzHilbert.PacketRepresentation.lineProjection_far_energy line 43
  4. theorem OAI.LipschitzHilbert.PacketRepresentation.outside_enlarged_interval_gap line 58