HomogeneousContourDomain.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Every finite contour vector lies in the actual generator domain

The bounded matrix generator differentiates the restricted semigroup. Its inclusion in Y × Y differentiates the original evolution, including vectors in nontrivial Jordan chains.

theorem OAI.DefocusingNLS.projectionSemigroup_generator_domain line 23

Source documentation

Differentiation of the matrix exponential commutes with the inclusion of the finite contour space in the ambient Banach space.

theorem projectionSemigroup_generator_domain (S : ℝ≥0 → E →L[ℂ] E)
    (Q : E →L[ℂ] E) (hcomm : ∀ t, Commute (S t) Q)
    (hfin : FiniteDimensional ℂ Q.range) (G : Q.range →L[ℂ] Q.range)
    (hG : ∀ t, projectionSemigroupRestriction S Q hcomm t =
      NormedSpace.exp ((t : ℝ) • G)) (w : Q.range) :
    HasDerivWithinAt (fun t : ℝ => S t.toNNReal (w : E))
      (G w : E) (Ici 0) 0 := by
…

Mentions: OAI.DefocusingNLS.projectionSemigroupRestriction

theorem OAI.DefocusingNLS.homogeneous_generator_free_coordinates line 52

Source documentation

Both real coordinates of an arbitrary complexified generator vector satisfy the exact bounded-potential perturbation identity.

theorem homogeneous_generator_free_coordinates (a b k : ℝ)
    (ha : 0 < a) (ha1 : a < 1) (hk : 8 < k) (m : ℕ) (q : HomogeneousY a k)
    (w z : HomogeneousY a k × HomogeneousY a k)
    (hw : HasDerivWithinAt (fun t : ℝ =>
      homogeneousComplexLinearizedStep a b k ha ha1 hk m q t.toNNReal w) z (Ici 0) 0) :
    let X := homogeneousComplexReal a k ha ha1 hk
…

Mentions: OAI.DefocusingNLS.HomogeneousY, OAI.DefocusingNLS.homogeneousComplexLinearizedStep, OAI.DefocusingNLS.homogeneousComplexReal