ExpandingNonlinearityTransport.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Continuity of the actual polynomial at a varying torus scale

The coefficient-preserving identification intertwines the exact Fourier products and conjugation. Thus the varying-scale nonlinearity is conjugate to the already smooth radius-one polynomial.

theorem OAI.DefocusingNLS.coefficient_injective line 17
Distinct definitions of this name: OAI/MathematicalPhysics/DefocusingNLS/Linear/ExpandingSobolevNonlinearity.lean:17 (different declaration text). Qualify references as OAI.DefocusingNLS.coefficient_injective@path.
theorem OAI.DefocusingNLS.expandingScaleTransfer_product line 24
theorem OAI.DefocusingNLS.expandingScaleTransfer_conjugate line 40
theorem OAI.DefocusingNLS.expandingScaleTransfer_oddPower line 49
theorem OAI.DefocusingNLS.transfer_inverse_apply line 61

theorem OAI.DefocusingNLS.expandingOddPower_transport line 69

Source documentation

Exact conjugation of the actual polynomial by the weight identification.

theorem expandingOddPower_transport (a k L : ℝ)
    (ha : 0 < a) (ha1 : a < 1) (hk : 8 < k) (hL : 1 ≤ L) (m : ℕ) (f : FourierL2) :
    expandingOddPower a k L ha ha1 hk hL m f =
      expandingScaleTransfer a k 1 L ha hk le_rfl hL
        (expandingOddPower a k 1 ha ha1 hk le_rfl m
          (expandingInverseTransfer a k L ha hk hL f)) := by
…

Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.expandingOddPower, OAI.DefocusingNLS.expandingScaleTransfer, OAI.DefocusingNLS.expandingInverseTransfer

theorem OAI.DefocusingNLS.continuous_expandingOddPower_scale line 78

Source documentation

The polynomial is jointly continuous in scale and input in the exact norms.

theorem continuous_expandingOddPower_scale (a k : ℝ)
    (ha : 0 < a) (ha1 : a < 1) (hk : 8 < k) (m : ℕ) :
    Continuous (fun p : {L : ℝ // 1 ≤ L} × FourierL2 =>
      expandingOddPower a k p.1.1 ha ha1 hk p.1.2 m p.2) := by
…

Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.expandingOddPower

theorem OAI.DefocusingNLS.fderiv_expandingOddPower_transport line 95

Source documentation

The linearization is the derivative of the same conjugated polynomial.

theorem fderiv_expandingOddPower_transport (a k L : ℝ)
    (ha : 0 < a) (ha1 : a < 1) (hk : 8 < k) (hL : 1 ≤ L)
    (m : ℕ) (q v : FourierL2) :
    fderiv ℝ (expandingOddPower a k L ha ha1 hk hL m) q v =
      expandingScaleTransfer a k 1 L ha hk le_rfl hL
        (fderiv ℝ (expandingOddPower a k 1 ha ha1 hk le_rfl m)
          (expandingInverseTransfer a k L ha hk hL q)
          (expandingInverseTransfer a k L ha hk hL v)) := by
…

Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.expandingOddPower, OAI.DefocusingNLS.expandingScaleTransfer, OAI.DefocusingNLS.expandingInverseTransfer

theorem OAI.DefocusingNLS.continuous_expandingLinearization_scale line 117

Source documentation

Joint strong continuity of the actual linearized potential in scale, profile and input.

theorem continuous_expandingLinearization_scale (a k : ℝ)
    (ha : 0 < a) (ha1 : a < 1) (hk : 8 < k) (m : ℕ) :
    Continuous (fun p : {L : ℝ // 1 ≤ L} × (FourierL2 × FourierL2) =>
      fderiv ℝ (expandingOddPower a k p.1.1 ha ha1 hk p.1.2 m) p.2.1 p.2.2) := by
…

Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.expandingOddPower