SourcePlanarPlancherel.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Product-coordinate Plancherel and the common-frequency witness needed for the actual planar packet Gram matrix.

abbrev OAI.LipschitzHilbert.HilbertPlane line 13
def OAI.LipschitzHilbert.liftPlanar line 15
theorem OAI.LipschitzHilbert.integral_hilbertPlane line 18
theorem OAI.LipschitzHilbert.fourier_liftPlanar line 24
def OAI.LipschitzHilbert.hilbertPlanarSchwartz line 35
Source documentation
Lift a planar Schwartz function to the Hilbert norm on the same coordinates.
```
def hilbertPlanarSchwartz (f : SchwartzMap (ℝ×ℝ) ℂ) : SchwartzMap (WithLp 2 (ℝ×ℝ)) ℂ :=
…
```
theorem OAI.LipschitzHilbert.hilbertPlanarSchwartz_apply line 38
theorem OAI.LipschitzHilbert.integral_hilbertPlanar_bridge line 41
theorem OAI.LipschitzHilbert.fourier_hilbertPlanar_bridge line 46

theorem OAI.LipschitzHilbert.planar_integral_inner_fourier line 51

Source documentation

Plancherel for the manuscript's product-coordinate Fourier transform.

theorem planar_integral_inner_fourier (f g : SchwartzMap (ℝ×ℝ) ℂ) :
    (∫ z, inner ℂ (planarFourier f z) (planarFourier g z) ∂volume.prod volume)=
      ∫ z, inner ℂ (f z) (g z) ∂volume.prod volume := by
…

Mentions: OAI.LipschitzHilbert.planarFourier

theorem OAI.LipschitzHilbert.planar_inner_eq_zero_of_disjoint line 64
theorem OAI.LipschitzHilbert.exists_common_angular_frequency line 76
Source documentation
Nonzero interaction gives an actual common angular frequency; no support-overlap premise is added to the packet estimate.
```
theorem exists_common_angular_frequency (f g : SchwartzMap (ℝ×ℝ) ℂ)
    (hinner : (∫ z, inner ℂ (f z) (g z) ∂volume.prod volume)≠0) :
    ∃ ξ η, planarAngularFourier f (ξ,η)≠0 ∧ planarAngularFourier g (ξ,η)≠0 := by
…
```
Mentions: OAI.LipschitzHilbert.planarAngularFourier