HomogeneousFiniteSemigroup.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Short-time averaging for the finite-dimensional semigroup

On a finite-dimensional invariant subspace, strong continuity is norm continuity. An invertible short-time integral then converts the semigroup identity into a differential equation. These are supporting lemmas for the actual contour subspace, with no spectral classification premise.

theorem OAI.DefocusingNLS.continuous_exists_unit_integral line 32
Source documentation
A continuous operator family starting at the identity has an invertible integral over some short positive interval.
```
theorem continuous_exists_unit_integral (f : ℝ → A) (hf : Continuous f)
    (hzero : f 0 = 1) :
    ∃ ε : ℝ, 0 < ε ∧ IsUnit (∫ s in (0 : ℝ)..ε, f s) := by
…
```

theorem OAI.DefocusingNLS.continuous_semigroup_integral_shift line 54

Source documentation

The integrated semigroup identity.

theorem continuous_semigroup_integral_shift (f : ℝ → A) (hf : Continuous f)
    (hmul : ∀ s t : ℝ, 0 ≤ s → 0 ≤ t → f (s + t) = f s * f t)
    {ε s : ℝ} (hε : 0 ≤ ε) (hs : 0 ≤ s) :
    f s * (∫ t in (0 : ℝ)..ε, f t) = ∫ t in s..s + ε, f t := by
…

theorem OAI.DefocusingNLS.continuous_semigroup_hasRightDerivative line 74

Source documentation

Norm continuity and the semigroup identity produce a bounded generator, without a differentiability hypothesis on the semigroup.

theorem continuous_semigroup_hasRightDerivative (f : ℝ → A) (hf : Continuous f)
    (hzero : f 0 = 1)
    (hmul : ∀ s t : ℝ, 0 ≤ s → 0 ≤ t → f (s + t) = f s * f t) :
    ∃ G : A, ∀ s : ℝ, 0 ≤ s →
      HasDerivWithinAt f (f s * G) (Ici s) s := by
…

theorem OAI.DefocusingNLS.continuous_semigroup_eq_exp line 112

Source documentation

The bounded generator obtained by averaging represents the semigroup by an exponential for every nonnegative time.

theorem continuous_semigroup_eq_exp (f : ℝ → A) (hf : Continuous f)
    (hzero : f 0 = 1)
    (hmul : ∀ s t : ℝ, 0 ≤ s → 0 ≤ t → f (s + t) = f s * f t) :
    ∃ G : A, ∀ t : ℝ, 0 ≤ t → f t = NormedSpace.exp (t • G) := by
…

theorem OAI.DefocusingNLS.finiteDimensional_semigroup_eq_exp line 150

Source documentation

Strongly continuous finite-dimensional semigroups are matrix exponentials; differentiability is a conclusion.

theorem finiteDimensional_semigroup_eq_exp (S : ℝ≥0 → E →L[ℂ] E)
    (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 : E →L[ℂ] E, ∀ t : ℝ≥0, S t = NormedSpace.exp ((t : ℝ) • G) := by
…