Intrinsic statement of Stone's generator relation

This file packages Stone's generator relation intrinsically, by the exact punctured-neighborhood difference-quotient domain and limit, without exposing the library's choice-based construction of the generator. It states Stone's theorem in both directions: every strongly continuous unitary group has a self-adjoint generator, and every self-adjoint operator generates such a group.

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

U has infinitesimal generator A: its domain is exactly the vectors whose Stone difference quotient converges, and the limit is A.

Equations

• One or more equations did not get rendered due to their size.

theorem stone_theorem_intrinsic {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] : (∀ (U : StrongContUnitary E), ∃ (A : E →ₗ.[ℂ] E), IsSelfAdjoint A ∧ U.Generates A) ∧ ∀ (A : E →ₗ.[ℂ] E), IsSelfAdjoint A → ∃ (U : StrongContUnitary E), U.Generates A

Stone's theorem in both directions: strongly continuous one-parameter unitary groups have self-adjoint generators, and every self-adjoint operator generates such a group.