OAI/Analysis/LipschitzHilbert/Fourier/NormalizedReverseConvolution.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Reverse disparity for the actual normalized finite convolution sum, with the constructed angular models and common lattice average.

  1. theorem OAI.LipschitzHilbert.PacketRepresentation.exists_normalized_reverse_convolution line 14