OAI/Analysis/LipschitzHilbert/Fourier/NormalizedBasicConvolution.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The basic packet bound applied to the actual finite sum of separated convolutions. The same bound holds for every translation and finite lattice subset, so the common probability average loses no row factor.

  1. theorem OAI.LipschitzHilbert.PacketRepresentation.exists_normalized_basic_convolution line 15