TorusDerivatives.lean`

22 declarations, 0 contain sorry, 0 declared as axioms

Coordinate derivatives of the torus Fourier series

For k>8, the continuous Fourier Laplacian agrees with the sum of the ordinary second derivatives along the twelve coordinate circles.

theorem OAI.DefocusingNLS.frequencyCoordinates_coe line 18
theorem OAI.DefocusingNLS.frequencyCoordinates_sq_sum line 23
theorem OAI.DefocusingNLS.frequencyCoordinates_sq_le line 28
theorem OAI.DefocusingNLS.frequencyCoordinates_abs_le line 34

def OAI.DefocusingNLS.torusCoordinateLine line 42

Source documentation

The real parameter t moves along the jth coordinate circle.

noncomputable def torusCoordinateLine (x : SchrodingerTorus) (j : Fin 12) (t : ℝ) :
    SchrodingerTorus := x + fun l => if l = j then (t : AddCircle (2 * Real.pi)) else 0

Mentions: OAI.DefocusingNLS.SchrodingerTorus

theorem OAI.DefocusingNLS.torusCoordinateLine_zero line 45
theorem OAI.DefocusingNLS.torusCharacter_add line 50
theorem OAI.DefocusingNLS.torusCharacter_coordinateLine line 55
theorem OAI.DefocusingNLS.hasDerivAt_torusCharacter_coordinateLine line 67
Source documentation
Each torus character has its expected coordinate derivative.
```
theorem hasDerivAt_torusCharacter_coordinateLine (n : frequencyLattice)
    (x : SchrodingerTorus) (j : Fin 12) (t : ℝ) :
    HasDerivAt (fun s => torusCharacter n (torusCoordinateLine x j s))
      (Complex.I * (frequencyCoordinates n j : ℂ) *
        torusCharacter n (torusCoordinateLine x j t)) t := by
…
```
Mentions: OAI.DefocusingNLS.frequencyLattice, OAI.DefocusingNLS.SchrodingerTorus, OAI.DefocusingNLS.torusCharacter, OAI.DefocusingNLS.torusCoordinateLine, OAI.DefocusingNLS.frequencyCoordinates
theorem OAI.DefocusingNLS.summable_quadratic_sobolev_coefficients line 79
theorem OAI.DefocusingNLS.summable_derivative_bound line 86
def OAI.DefocusingNLS.torusPartial line 94
Source documentation
First coordinate derivative, represented by its absolutely convergent Fourier series.
```
noncomputable def torusPartial (k : ℝ) (f : FourierL2) (j : Fin 12)
    (x : SchrodingerTorus) : ℂ :=
…
```
Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.SchrodingerTorus
def OAI.DefocusingNLS.torusSecondPartial line 100
Source documentation
Second coordinate derivative, represented by its absolutely convergent Fourier series.
```
noncomputable def torusSecondPartial (k : ℝ) (f : FourierL2) (j : Fin 12)
    (x : SchrodingerTorus) : ℂ :=
…
```
Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.SchrodingerTorus
lemma OAI.DefocusingNLS.torusPartial_term_bound line 105
lemma OAI.DefocusingNLS.torusSecondPartial_term_bound line 113
theorem OAI.DefocusingNLS.hasDerivAt_torusFunction_coordinateLine line 122
Source documentation
Termwise differentiation of the Fourier series gives the actual first coordinate derivative.
```
theorem hasDerivAt_torusFunction_coordinateLine (k : ℝ) (hk : 8 < k) (f : FourierL2)
    (x : SchrodingerTorus) (j : Fin 12) (t : ℝ) :
    HasDerivAt (fun s => sobolevTorusFunction k f (torusCoordinateLine x j s))
      (torusPartial k f j (torusCoordinateLine x j t)) t := by
…
```
Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.SchrodingerTorus, OAI.DefocusingNLS.torusCoordinateLine, OAI.DefocusingNLS.torusPartial
theorem OAI.DefocusingNLS.hasDerivAt_torusPartial_coordinateLine line 145
Source documentation
The derivative of the first coordinate derivative is the stated second series.
```
theorem hasDerivAt_torusPartial_coordinateLine (k : ℝ) (hk : 8 < k) (f : FourierL2)
    (x : SchrodingerTorus) (j : Fin 12) (t : ℝ) :
    HasDerivAt (fun s => torusPartial k f j (torusCoordinateLine x j s))
      (torusSecondPartial k f j (torusCoordinateLine x j t)) t := by
…
```
Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.SchrodingerTorus, OAI.DefocusingNLS.torusPartial, OAI.DefocusingNLS.torusCoordinateLine, OAI.DefocusingNLS.torusSecondPartial
theorem OAI.DefocusingNLS.sum_torusSecondPartial_eq_laplacian line 166
Source documentation
The ordinary coordinate Laplacian equals the continuous spectral Laplacian.
```
theorem sum_torusSecondPartial_eq_laplacian (k : ℝ) (hk : 8 < k) (f : FourierL2)
    (x : SchrodingerTorus) :
    ∑ j : Fin 12, torusSecondPartial k f j x = torusFourierLaplacian k f x := by
…
```
Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.SchrodingerTorus, OAI.DefocusingNLS.torusSecondPartial, OAI.DefocusingNLS.torusFourierLaplacian
theorem OAI.DefocusingNLS.torusFunction_first_derivative line 183
theorem OAI.DefocusingNLS.torusFunction_second_derivative line 189
theorem OAI.DefocusingNLS.sum_coordinate_second_derivative_eq_laplacian line 200
Source documentation
The Fourier Laplacian is the sum of the ordinary coordinate second derivatives.
```
theorem sum_coordinate_second_derivative_eq_laplacian (k : ℝ) (hk : 8 < k)
    (f : FourierL2) (x : SchrodingerTorus) :
    ∑ j : Fin 12,
      deriv (deriv (fun s => sobolevTorusFunction k f (torusCoordinateLine x j s))) 0 =
      torusFourierLaplacian k f x := by
…
```
Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.SchrodingerTorus, OAI.DefocusingNLS.torusCoordinateLine, OAI.DefocusingNLS.torusFourierLaplacian

theorem OAI.DefocusingNLS.freeTorusEvolution_schrodinger_equation line 209

Source documentation

The free evolution solves i∂ₜu+Δu=0 with the ordinary torus Laplacian.

theorem freeTorusEvolution_schrodinger_equation (k : ℝ) (hk : 8 < k)
    (f : FourierL2) (x : SchrodingerTorus) (t : ℝ) :
    Complex.I * deriv (fun s => freeTorusEvolution k f s x) t +
      ∑ j : Fin 12,
        deriv (deriv (fun s => freeTorusEvolution k f t (torusCoordinateLine x j s))) 0 = 0 := by
…

Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.SchrodingerTorus, OAI.DefocusingNLS.freeTorusEvolution, OAI.DefocusingNLS.torusCoordinateLine