SobolevConvolution.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

Weighted convolution for Sobolev multiplication

The frequency weight inequality and Young's inequality give an explicit ℓ² majorant for the Fourier coefficients of a product.

theorem OAI.DefocusingNLS.weight_mul_sobolevFourierCoefficient line 18
theorem OAI.DefocusingNLS.weight_mul_norm_sobolevFourierCoefficient line 28
theorem OAI.DefocusingNLS.norm_sobolevFourierCoefficient_le line 35
def OAI.DefocusingNLS.sobolevProductCoefficient line 47
Source documentation
The physical coefficients of the product are the discrete convolution.
Also declared: ComparatorChallenges/DefocusingNLS.lean:101 (same declaration text).
```
noncomputable def sobolevProductCoefficient (k : ℝ) (f g : FourierL2)
    (n : frequencyLattice) : ℂ :=
…
```
Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.frequencyLattice
theorem OAI.DefocusingNLS.summable_norm_sobolevProductTerms line 51
theorem OAI.DefocusingNLS.absolute_convolution_apply line 60
def OAI.DefocusingNLS.sobolevProductMajorant line 68
Source documentation
The two unweighted Young convolutions which dominate the weighted product.
```
noncomputable def sobolevProductMajorant (k : ℝ) (f g : FourierL2) : FourierL2 :=
…
```
Mentions: OAI.DefocusingNLS.FourierL2
theorem OAI.DefocusingNLS.sobolevProductMajorant_norm_apply line 73
lemma OAI.DefocusingNLS.weighted_product_term_bound line 88
theorem OAI.DefocusingNLS.weighted_sobolevProduct_le_majorant line 107
Source documentation
The weighted convolution is bounded pointwise by an ℓ² vector.
```
theorem weighted_sobolevProduct_le_majorant (k : ℝ) (hk : 6 < k) (f g : FourierL2)
    (n : frequencyLattice) :
    ‖(sobolevProductWeight k n : ℂ) * sobolevProductCoefficient k f g n‖ ≤
      ‖sobolevProductMajorant k f g n‖ := by
…
```
Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.frequencyLattice, OAI.DefocusingNLS.sobolevProductCoefficient, OAI.DefocusingNLS.sobolevProductMajorant
def OAI.DefocusingNLS.sobolevProduct line 148
Source documentation
Multiplication closes in the original Sobolev Fourier space.
Distinct definitions of this name: ComparatorChallenges/DefocusingNLS.lean:105 (different declaration text). Qualify references as OAI.DefocusingNLS.sobolevProduct@path.
```
noncomputable def sobolevProduct (k : ℝ) (hk : 6 < k) (f g : FourierL2) : FourierL2 :=
…
```
Mentions: OAI.DefocusingNLS.FourierL2
theorem OAI.DefocusingNLS.sobolevProduct_coefficient line 153
theorem OAI.DefocusingNLS.sobolevProductMajorant_norm_le line 162
Source documentation
A quantitative norm bound for the two-Young-convolution majorant.
```
theorem sobolevProductMajorant_norm_le (k : ℝ) (hk : 6 < k) (f g : FourierL2) :
    ‖sobolevProductMajorant k f g‖ ≤
      2 * 4 ^ (k / 2) * ‖sobolevObservationVector k hk‖ * ‖f‖ * ‖g‖ := by
…
```
Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.sobolevProductMajorant, OAI.DefocusingNLS.sobolevObservationVector
theorem OAI.DefocusingNLS.sobolevProduct_norm_le line 196
Source documentation
Multiplication is bounded bilinearly in the twelve-dimensional Sobolev norm.
```
theorem sobolevProduct_norm_le (k : ℝ) (hk : 6 < k) (f g : FourierL2) :
    ‖sobolevProduct k hk f g‖ ≤
      2 * 4 ^ (k / 2) * ‖sobolevObservationVector k hk‖ * ‖f‖ * ‖g‖ := by
…
```
Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.sobolevObservationVector