OAI/Analysis/LipschitzHilbert/Fourier/FiniteNormalizedKernelForm.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The exact finite convolution form is realized on the arbitrary retained subset of the common translated spatial lattices.

  1. theorem OAI.LipschitzHilbert.PacketRepresentation.finite_normalized_kernel_form line 27