OAI/Analysis/LipschitzHilbert/Estimates/LocalizedSubbandOperator.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A bound for an enlarged band controls every subband, with the norm of the projected input. Horizontal localization commutes with projections.

  1. def OAI.LipschitzHilbert.PacketRepresentation.localizedSharpOperator line 14
  2. theorem OAI.LipschitzHilbert.PacketRepresentation.verticalL2Projection_strip line 22
  3. theorem OAI.LipschitzHilbert.PacketRepresentation.localizedSharpBandOperator_subband line 27
  4. theorem OAI.LipschitzHilbert.PacketRepresentation.localizedSharpOperator_subband_bound line 40