OAI/Analysis/LipschitzHilbert/Estimates/ShortSlopeOperator.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The short-time frozen-direction operator and the exact reason it may replace the full kernel in a pairing on a narrow horizontal strip.

  1. def OAI.LipschitzHilbert.PacketRepresentation.shortSlopeOperator line 12
  2. theorem OAI.LipschitzHilbert.PacketRepresentation.shortSlopeOperator_measurable line 16
  3. theorem OAI.LipschitzHilbert.PacketRepresentation.shortSlopeOperator_energy line 27
  4. theorem OAI.LipschitzHilbert.PacketRepresentation.shortSlopeOperator_pairing_eq line 58