SobolevMultiplication.lean`

17 declarations, 0 contain sorry, 0 declared as axioms

Sobolev multiplication agrees with pointwise multiplication on the torus

theorem OAI.DefocusingNLS.frequencyCoordinates_add line 11
theorem OAI.DefocusingNLS.torusCharacter_frequency_add line 17
def OAI.DefocusingNLS.frequencySumEquiv line 24
Source documentation
The additive shear used to collect terms of a double Fourier series.
```
noncomputable def frequencySumEquiv : frequencyLattice × frequencyLattice ≃
    frequencyLattice × frequencyLattice where
…
```
Mentions: OAI.DefocusingNLS.frequencyLattice

theorem OAI.DefocusingNLS.tsum_frequency_convolution line 32

Source documentation

Collect an absolutely convergent double series by the sum of its frequencies.

theorem tsum_frequency_convolution (a b : frequencyLattice → ℂ)
    (ha : Summable (fun n => ‖a n‖)) (hb : Summable (fun n => ‖b n‖)) :
    (∑' n, a n) * (∑' n, b n) = ∑' n, ∑' m, a m * b (n - m) := by
…

Mentions: OAI.DefocusingNLS.frequencyLattice

theorem OAI.DefocusingNLS.tsum_fourier_product line 49

Source documentation

The absolutely convergent Fourier Cauchy product on the actual torus.

theorem tsum_fourier_product (a b : frequencyLattice → ℂ)
    (ha : Summable (fun n => ‖a n‖)) (hb : Summable (fun n => ‖b n‖))
    (x : SchrodingerTorus) :
    (∑' n, a n * torusCharacter n x) * (∑' n, b n * torusCharacter n x) =
      ∑' n, (∑' m, a m * b (n - m)) * torusCharacter n x := by
…

Mentions: OAI.DefocusingNLS.frequencyLattice, OAI.DefocusingNLS.SchrodingerTorus, OAI.DefocusingNLS.torusCharacter

lemma OAI.DefocusingNLS.sobolevTorusFunction_eq_tsum line 68

theorem OAI.DefocusingNLS.sobolevTorusFunction_product line 76

Source documentation

The bounded Sobolev product is exactly the usual product of torus functions.

theorem sobolevTorusFunction_product (k : ℝ) (hk : 6 < k) (f g : FourierL2) :
    sobolevTorusFunction k (sobolevProduct k hk f g) =
      sobolevTorusFunction k f * sobolevTorusFunction k g := by
…

Mentions: OAI.DefocusingNLS.FourierL2

lemma OAI.DefocusingNLS.sobolevFourierCoefficient_add line 86
lemma OAI.DefocusingNLS.sobolevFourierCoefficient_smul line 91
lemma OAI.DefocusingNLS.summable_sobolevProductTerms line 97
theorem OAI.DefocusingNLS.sobolevProduct_comm line 103
theorem OAI.DefocusingNLS.sobolevProduct_add_left line 114
theorem OAI.DefocusingNLS.sobolevProduct_smul_left line 126
theorem OAI.DefocusingNLS.sobolevProduct_add_right line 135
theorem OAI.DefocusingNLS.sobolevProduct_smul_right line 140
def OAI.DefocusingNLS.sobolevBilinearProduct line 145
Source documentation
The usual torus product is a continuous complex-bilinear operation in H^k.
```
noncomputable def sobolevBilinearProduct (k : ℝ) (hk : 6 < k) :
    FourierL2 →L[ℂ] FourierL2 →L[ℂ] FourierL2 :=
…
```
Mentions: OAI.DefocusingNLS.FourierL2
theorem OAI.DefocusingNLS.sobolevBilinearProduct_apply line 152