OAI/Analysis/LipschitzHilbert/Estimates/FiniteBinCommutator.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The integrated bin commutator for the actual finite dyadic time kernel. The bound is uniform in the number of scales and in the bin carrier.

  1. def OAI.LipschitzHilbert.PacketRepresentation.finiteBinError line 12
  2. theorem OAI.LipschitzHilbert.PacketRepresentation.finiteBinCommutator_energy line 17