FourierAveragingKernel.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

A positive averaging kernel with compact Fourier support

Square the norm of the Fourier transform of a smooth compactly supported bump. Plancherel converts its Fourier moments into overlaps of translates of the bump; disjoint supports therefore give exact annihilation.

def OAI.LipschitzHilbert.fourierSquare line 26
Source documentation
The nonnegative physical-space averaging density before normalization.
```
def fourierSquare (h : SchwartzMap ℝ ℂ) (t : ℝ) : ℝ := ‖𝓕 h t‖ ^ 2
```
theorem OAI.LipschitzHilbert.schwartz_norm_sq_integrable line 28
theorem OAI.LipschitzHilbert.fourierSquare_integrable line 35
theorem OAI.LipschitzHilbert.fourierSquare_nonneg line 38
theorem OAI.LipschitzHilbert.fourierSquare_continuous line 40

theorem OAI.LipschitzHilbert.schwartz_fourier_translate line 44

Source documentation

Translation on the compact-frequency side becomes a unit phase.

theorem schwartz_fourier_translate (h : SchwartzMap ℝ ℂ) (a x : ℝ) :
    𝓕 (h.compSubConstCLM ℂ (-a)) x = character (2 * Real.pi * a) x * 𝓕 h x := by
…

theorem OAI.LipschitzHilbert.fourierSquare_moment line 59
Source documentation
The Fourier moment of the square is an overlap integral of the bump and its translate. This is the exact support calculation needed for averaging.
```
theorem fourierSquare_moment (h : SchwartzMap ℝ ℂ) (a : ℝ) :
    (∫ t, (fourierSquare h t : ℂ) * character (2 * Real.pi * a) t) =
      ∫ x, inner ℂ (h x) (h (x + a)) := by
…
```
Mentions: OAI.LipschitzHilbert.fourierSquare
theorem OAI.LipschitzHilbert.fourierSquare_moment_eq_zero line 76
Source documentation
A bump supported in (-r,r) produces no moment at translation distances at least 2r, including the support endpoints.
```
theorem fourierSquare_moment_eq_zero (h : SchwartzMap ℝ ℂ) {r a : ℝ}
    (hsupport : ∀ x, r ≤ |x| → h x = 0) (ha : 2 * r ≤ |a|) :
    (∫ t, (fourierSquare h t : ℂ) * character (2 * Real.pi * a) t) = 0 := by
…
```
Mentions: OAI.LipschitzHilbert.fourierSquare
theorem OAI.LipschitzHilbert.fourierSquare_mass_pos line 94
Source documentation
The total mass is positive whenever the original bump is nonzero at one point, and agrees with its squared L2 norm by Plancherel.
```
theorem fourierSquare_mass_pos (h : SchwartzMap ℝ ℂ) {x : ℝ} (hx : h x ≠ 0) :
    0 < ∫ t, fourierSquare h t := by
…
```
Mentions: OAI.LipschitzHilbert.fourierSquare