ExpandingConvolution.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Multiplication with the exact expanding-torus Fourier weight

The constants below are independent of the expanding radius L.

theorem OAI.DefocusingNLS.weight_mul_norm_expandingFourierCoefficient line 15
theorem OAI.DefocusingNLS.norm_expandingFourierCoefficient_le line 22
def OAI.DefocusingNLS.expandingProductCoefficient line 34
Source documentation
The physical coefficients of the product are the discrete convolution.
```
noncomputable def expandingProductCoefficient (a k L : ℝ) (f g : FourierL2)
    (n : frequencyLattice) : ℂ :=
…
```
Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.frequencyLattice
theorem OAI.DefocusingNLS.summable_norm_expandingProductTerms line 38
def OAI.DefocusingNLS.expandingProductMajorant line 48
Source documentation
The two unweighted Young convolutions which dominate the weighted product.
```
noncomputable def expandingProductMajorant (a k L : ℝ) (f g : FourierL2) : FourierL2 :=
…
```
Mentions: OAI.DefocusingNLS.FourierL2
theorem OAI.DefocusingNLS.expandingProductMajorant_norm_apply line 53
lemma OAI.DefocusingNLS.expanding_weighted_product_term_bound line 68
theorem OAI.DefocusingNLS.weighted_expandingProduct_le_majorant line 87
Source documentation
The weighted convolution is bounded pointwise by an ℓ² vector.
```
theorem weighted_expandingProduct_le_majorant (a k L : ℝ) (ha : 0 < a) (ha1 : a < 1) (hk : 8 < k) (hL : 1 ≤ L) (f g : FourierL2)
    (n : frequencyLattice) :
    ‖(expandingSobolevWeight a k L n : ℂ) * expandingProductCoefficient a k L f g n‖ ≤
      ‖expandingProductMajorant a k L f g n‖ := by
…
```
Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.frequencyLattice, OAI.DefocusingNLS.expandingSobolevWeight, OAI.DefocusingNLS.expandingProductCoefficient, OAI.DefocusingNLS.expandingProductMajorant
def OAI.DefocusingNLS.expandingProduct line 128
Source documentation
Multiplication closes with the exact expanding-torus Fourier weight.
```
noncomputable def expandingProduct (a k L : ℝ) (ha : 0 < a) (ha1 : a < 1) (hk : 8 < k) (hL : 1 ≤ L) (f g : FourierL2) : FourierL2 :=
…
```
Mentions: OAI.DefocusingNLS.FourierL2
theorem OAI.DefocusingNLS.expandingProduct_coefficient line 133
theorem OAI.DefocusingNLS.expandingProductMajorant_norm_le line 142
Source documentation
A quantitative norm bound for the two-Young-convolution majorant.
```
theorem expandingProductMajorant_norm_le (a k L : ℝ) (ha : 0 < a) (ha1 : a < 1) (hk : 8 < k) (hL : 1 ≤ L) (f g : FourierL2) :
    ‖expandingProductMajorant a k L f g‖ ≤
      2 * Real.sqrt (4 ^ k) * expandingEmbeddingBound a k * ‖f‖ * ‖g‖ := by
…
```
Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.expandingProductMajorant, OAI.DefocusingNLS.expandingEmbeddingBound

theorem OAI.DefocusingNLS.expandingProduct_norm_le line 176

Source documentation

The Y_L multiplication constant is independent of L ≥ 1.

theorem expandingProduct_norm_le (a k L : ℝ) (ha : 0 < a) (ha1 : a < 1) (hk : 8 < k) (hL : 1 ≤ L) (f g : FourierL2) :
    ‖expandingProduct a k L ha ha1 hk hL f g‖ ≤
      2 * Real.sqrt (4 ^ k) * expandingEmbeddingBound a k * ‖f‖ * ‖g‖ := by
…

Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.expandingProduct, OAI.DefocusingNLS.expandingEmbeddingBound