FourierConvolution.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Young's inequality for the Fourier lattice

An absolutely summable coefficient sequence convolves boundedly with an ℓ² sequence. The proof sums translated ℓ² vectors, so no external convolution estimate is assumed.

def OAI.DefocusingNLS.fourierTranslateVector line 19
Source documentation
A Fourier vector with its indices shifted by m.
```
noncomputable def fourierTranslateVector (m : frequencyLattice) (f : FourierL2) : FourierL2 :=
…
```
Mentions: OAI.DefocusingNLS.frequencyLattice, OAI.DefocusingNLS.FourierL2
theorem OAI.DefocusingNLS.fourierTranslateVector_apply line 25
theorem OAI.DefocusingNLS.fourierTranslateVector_norm line 28
def OAI.DefocusingNLS.fourierTranslation line 39
Source documentation
Translation of Fourier indices is a complex-linear isometry.
```
noncomputable def fourierTranslation (m : frequencyLattice) : FourierL2 →ₗᵢ[ℂ] FourierL2 where
…
```
Mentions: OAI.DefocusingNLS.frequencyLattice, OAI.DefocusingNLS.FourierL2
theorem OAI.DefocusingNLS.fourierTranslation_apply line 45
def OAI.DefocusingNLS.fourierConvolution line 49
Source documentation
Discrete convolution, formed as an ℓ²-valued absolutely convergent series.
```
noncomputable def fourierConvolution (a : frequencyLattice → ℂ) (f : FourierL2) : FourierL2 :=
…
```
Mentions: OAI.DefocusingNLS.frequencyLattice, OAI.DefocusingNLS.FourierL2
theorem OAI.DefocusingNLS.summable_fourierConvolution_terms line 52
theorem OAI.DefocusingNLS.fourierConvolution_apply line 59
Source documentation
The ℓ²-valued construction agrees with the usual coefficient convolution.
```
theorem fourierConvolution_apply (a : frequencyLattice → ℂ)
    (ha : Summable (fun m => ‖a m‖)) (f : FourierL2) (n : frequencyLattice) :
    fourierConvolution a f n = ∑' m, a m * f (n - m) := by
…
```
Mentions: OAI.DefocusingNLS.frequencyLattice, OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.fourierConvolution
theorem OAI.DefocusingNLS.fourierConvolution_norm_le line 67
Source documentation
Young's ℓ¹ * ℓ² → ℓ² inequality on the twelve-dimensional lattice.
```
theorem fourierConvolution_norm_le (a : frequencyLattice → ℂ)
    (ha : Summable (fun m => ‖a m‖)) (f : FourierL2) :
    ‖fourierConvolution a f‖ ≤ (∑' m, ‖a m‖) * ‖f‖ := by
…
```
Mentions: OAI.DefocusingNLS.frequencyLattice, OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.fourierConvolution