OAI/Analysis/LipschitzHilbert/Fourier/DominatedKernelAverage.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A time kernel may depend measurably on the output point. An integrable scalar majorant still gives the same elementary L2 averaging bound.

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