OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousPotentialPicard.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Whole-space mild evolution for a bounded real-linear potential

The construction acts on the faithful homogeneous Fourier completion and takes a bounded real operator as input. Identifying the manuscript profile potential with such an operator is a separate spatial estimate.

  1. def OAI.DefocusingNLS.homogeneousPotentialHistory line 23
  2. theorem OAI.DefocusingNLS.continuous_homogeneousPotentialHistory line 28
  3. def OAI.DefocusingNLS.homogeneousTimeWeight line 34
  4. theorem OAI.DefocusingNLS.homogeneousTimeWeight_cancel line 40
  5. def OAI.DefocusingNLS.homogeneousPotentialPicard line 49
  6. def OAI.DefocusingNLS.homogeneousPotentialBielecki line 60
  7. theorem OAI.DefocusingNLS.homogeneousPotentialBielecki_dist_le line 68

    Source documentation

    The contraction constant is independent of the finite slab length.

    theorem homogeneousPotentialBielecki_dist_le (a b k T η : ℝ)
    (ha : 0 < a) (ha1 : a < 1) (hk : 8 < k) (hT : 0 ≤ T) (hη : 0 < η)
    (B : HomogeneousY a k →L[ℝ] HomogeneousY a k) (u₀ : HomogeneousY a k)
    (u v : C(Icc (0 : ℝ) T, HomogeneousY a k)) :
    dist (homogeneousPotentialBielecki a b k T η ha ha1 hk hT B u₀ u)
      (homogeneousPotentialBielecki a b k T η ha ha1 hk hT B u₀ v) ≤ ‖B‖ / η * dist u v := by
…

    Mentions: OAI.DefocusingNLS.HomogeneousY, OAI.DefocusingNLS.homogeneousPotentialBielecki

  8. theorem OAI.DefocusingNLS.existsUnique_homogeneousPotential_finiteSlab line 107

    Source documentation

    A bounded real-linear perturbation has one mild trajectory on every finite forward slab.

    theorem existsUnique_homogeneousPotential_finiteSlab (a b k T : ℝ)
    (ha : 0 < a) (ha1 : a < 1) (hk : 8 < k) (hT : 0 ≤ T)
    (B : HomogeneousY a k →L[ℝ] HomogeneousY a k) (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 B u) := by
…

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