OAI/Analysis/LipschitzHilbert/Estimates/PlanarSeparatedEnergy.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Orthogonality of separated reference-frequency strips on the plane. The proof uses the actual Fourier transform of each affine line slice, then integrates the one-dimensional Plancherel identity.

  1. theorem OAI.LipschitzHilbert.schwartz_energy_fourier_disjoint line 15
  2. theorem OAI.LipschitzHilbert.planar_energy_of_slice_fourier_disjoint line 36
  3. theorem OAI.LipschitzHilbert.planar_separated_strip_energy line 74
  4. theorem OAI.LipschitzHilbert.planar_separated_strip_vector_energy line 102