OAI/Analysis/LipschitzHilbert/Estimates/SeparatedPlanarSynthesis.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Combining the box-lattice synthesis bound with separated annuli. This is the nonmaximal, unweighted separated synthesis estimate of §3, including the dimension-independent sum over frequency bins.

  1. theorem OAI.LipschitzHilbert.planarFourier_finsetSum line 16
  2. theorem OAI.LipschitzHilbert.separated_planar_synthesis_energy line 26