HomogeneousInvariantSemigroup.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Restriction to the finite-dimensional contour space

A projection commuting with the actual evolution has an invariant range. Strong continuity therefore gives a matrix generator on that range.

instance OAI.DefocusingNLS.projectionRangeEnd_isTopologicalRing line 23
Source documentation
Explicit topological-ring structure for endomorphisms of the projection range.
```
instance projectionRangeEnd_isTopologicalRing (Q : E →L[ℂ] E) :
    IsTopologicalRing (Q.range →L[ℂ] Q.range) :=
…
```
theorem OAI.DefocusingNLS.projection_range_invariant line 27
def OAI.DefocusingNLS.projectionSemigroupRestriction line 33
theorem OAI.DefocusingNLS.projectionSemigroupRestriction_apply line 38

theorem OAI.DefocusingNLS.projectionSemigroupRestriction_eq_exp line 45

Source documentation

The finite contour space of a strongly continuous semigroup has an actual matrix generator.

theorem projectionSemigroupRestriction_eq_exp
    (S : ℝ≥0 → E →L[ℂ] E) (Q : E →L[ℂ] E)
    (hcomm : ∀ t, Commute (S t) Q)
    (hfin : FiniteDimensional ℂ Q.range)
    (hS : ∀ x : E, Continuous (fun t => S t x)) (hzero : S 0 = 1)
    (hadd : ∀ s t : ℝ≥0, S (s + t) = S t * S s) :
    ∃ G : Q.range →L[ℂ] Q.range, ∀ t : ℝ≥0,
      projectionSemigroupRestriction S Q hcomm t =
        NormedSpace.exp ((t : ℝ) • G) := by
…

Mentions: OAI.DefocusingNLS.projectionSemigroupRestriction