Strongly continuous unitary groups and their generators

This file defines strongly continuous one-parameter unitary groups and the infinitesimal-generator relation between such a group and a partial operator, via the Stone difference quotient.

structure StrongContUnitary (E : Type u_2) [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] : Type u_2

A strongly continuous one-parameter unitary group.

• toFun : ℝ → E →L[ℂ] E

  The unitary operator at each real time.

• isUnitary (t : ℝ) : self.toFun t ∈ unitary (E →L[ℂ] E)
• zero : self.toFun 0 = 1
• add (s t : ℝ) : self.toFun (s + t) = self.toFun s * self.toFun t
• stronglyContinuous (x : E) : Continuous fun (t : ℝ) => (self.toFun t) x

noncomputable def StrongContUnitary.differenceQuotient {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (U : StrongContUnitary E) (x : E) (t : ℝ) : E

The difference quotient (U(t)x - x) / (i * t) of the unitary group.

Equations

• U.differenceQuotient x t = (Complex.I * ↑t)⁻¹ • ((U.toFun t) x - x)

def StrongContUnitary.generatorDomain {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (U : StrongContUnitary E) : Submodule ℂ E

The vectors whose difference quotient converges at zero through nonzero times.

Equations

• U.generatorDomain = { carrier := {x : E | ∃ (y : E), Filter.Tendsto (U.differenceQuotient x) (nhdsWithin 0 {0}ᶜ) (nhds y)}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

noncomputable def StrongContUnitary.generatorLimit {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (U : StrongContUnitary E) (x : ↥U.generatorDomain) : E

The chosen limit of the difference quotient on the generator domain.

Equations

• U.generatorLimit x = Classical.choose ⋯

noncomputable def StrongContUnitary.generator {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (U : StrongContUnitary E) : E →ₗ.[ℂ] E

The infinitesimal generator of a strongly continuous unitary group.

Its domain consists of the vectors for which (U(t)x - x) / (i * t) converges as nonzero real t tends to zero.

Equations

• U.generator = { domain := U.generatorDomain, toFun := { toFun := U.generatorLimit, map_add' := ⋯, map_smul' := ⋯ } }

theorem StrongContUnitary.mem_generator_domain_iff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (U : StrongContUnitary E) (x : E) : x ∈ U.generator.domain ↔ ∃ (y : E), Filter.Tendsto (fun (t : ℝ) => (Complex.I * ↑t)⁻¹ • ((U.toFun t) x - x)) (nhdsWithin 0 {0}ᶜ) (nhds y)

Membership in the generator domain is convergence of the Stone difference quotient.

theorem StrongContUnitary.tendsto_generator {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (U : StrongContUnitary E) (x : ↥U.generator.domain) : Filter.Tendsto (fun (t : ℝ) => (Complex.I * ↑t)⁻¹ • ((U.toFun t) ↑x - ↑x)) (nhdsWithin 0 {0}ᶜ) (nhds (↑U.generator x))

On its domain, the Stone difference quotient converges to the generator.