OAI/NumberTheory/Ostmann/Characters/PublishedBonami.lean

Published finite-cube hypercontractive input

A. Bonami, Étude des coefficients de Fourier des fonctions de Lᵖ(G), Annales de l'Institut Fourier 20 (1970), no. 2, 335–402, Chapter III, Theorems 2–3, printed pp. 374–376. DOI: 10.5802/aif.357; https://www.numdam.org/item/10.5802/aif.357.pdf .

PublishedBonamiBound is only the real finite Boolean-cube consequence with p=2 and q=2l: applying the noise operator with multiplier (2l-1)^(-card Q/2) gives this weighted even-moment inequality. This is an explicit hypothesis, not a global axiom. No assertion about primes, Jacobi symbols, translating residues or the target sumset is included in it.