HomogeneousLinearization.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Actual pointwise linearized potential on the homogeneous space

def OAI.DefocusingNLS.homogeneousPointEvaluation line 15
theorem OAI.DefocusingNLS.homogeneousOddPower_fderiv_physical line 24
def OAI.DefocusingNLS.homogeneousLinearizedPotential line 47
Source documentation
The Schrödinger linearization is a bounded real operator on the actual Y space.
```
noncomputable def homogeneousLinearizedPotential (a k : ℝ)
    (ha : 0 < a) (ha1 : a < 1) (hk : 8 < k) (m : ℕ) (q : HomogeneousY a k) :
    HomogeneousY a k →L[ℝ] HomogeneousY a k :=
…
```
Mentions: OAI.DefocusingNLS.HomogeneousY
theorem OAI.DefocusingNLS.homogeneousLinearizedPotential_physical line 52

theorem OAI.DefocusingNLS.existsUnique_homogeneousLinearized_finiteSlab line 62

Source documentation

The previously constructed finite-slab flow applies to the actual profile linearization.

theorem existsUnique_homogeneousLinearized_finiteSlab (a b k T : ℝ)
    (ha : 0 < a) (ha1 : a < 1) (hk : 8 < k) (hT : 0 ≤ T) (m : ℕ)
    (q u₀ : HomogeneousY a k) :
    ∃! u : C(Icc (0 : ℝ) T, HomogeneousY a k), ∀ t : Icc (0 : ℝ) T,
      u t = homogeneousFreeOperator a b k t ha ha1 hk u₀ +
        homogeneousDuhamel a b k ha ha1 hk t
          (homogeneousPotentialHistory T hT (homogeneousLinearizedPotential a k ha ha1 hk m q) u) :=
…

Mentions: OAI.DefocusingNLS.HomogeneousY, OAI.DefocusingNLS.homogeneousFreeOperator, OAI.DefocusingNLS.homogeneousDuhamel, OAI.DefocusingNLS.homogeneousPotentialHistory, OAI.DefocusingNLS.homogeneousLinearizedPotential