OAI/Analysis/LipschitzHilbert/Fourier/DyadicAnnularSeparation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A fixed number of residue classes separates the dyadic annuli in the ordinary synthesis estimate. The number depends only on the two fixed annular constants, independently of the number of scales.

  1. theorem OAI.LipschitzHilbert.exists_dyadic_annular_separation line 14