OAI/Analysis/LipschitzHilbert/Estimates/PlanarFixedScaleEnergy.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The fixed-length synthesis estimate in section 3. A single translated box lattice has bounded overlap. Summing squared bin components gives a constant independent of the number of packets and frequency bins.

  1. def OAI.LipschitzHilbert.planarFixedSynthesis line 16
  2. theorem OAI.LipschitzHilbert.planarFixedSynthesis_memLp line 21
  3. theorem OAI.LipschitzHilbert.planarFixedSynthesis_pointwise line 28
  4. theorem OAI.LipschitzHilbert.planar_envelope_integrable line 44
  5. theorem OAI.LipschitzHilbert.integral_planar_envelope line 52
  6. theorem OAI.LipschitzHilbert.planar_fixed_scale_energy line 69