OAI/Analysis/LipschitzHilbert/Fourier/LatticeCoefficientConvolution.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Actual analyzing coefficients controlled by a common scalar source satisfy the fixed-scale positive convolution estimate.

  1. theorem OAI.LipschitzHilbert.lattice_coefficient_convolution line 15