OAI/Analysis/LipschitzHilbert/Fourier/KernelAverageEnergy.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

An energy bound for a time average of a uniformly bounded family. This is used with the time-normalized sampling commutator.

  1. theorem OAI.LipschitzHilbert.PacketRepresentation.kernelAverage_energy line 11