The Dyson series of a continuous path in a Banach algebra

For a continuous path p : ℝ → B in a real Banach algebra, the time-ordered exponential Γ t is the solution of the linear equation Γ' t = Γ t * p t with Γ 0 = 1. It is given by the norm-convergent Dyson series of iterated integrals

Γ t = 1 + ∫₀ᵗ p s₁ ds₁ + ∫₀ᵗ ∫₀^{s₂} p s₁ * p s₂ ds₁ ds₂ + ⋯,

whose n-th term is bounded by ‖1‖ (C |t|)ⁿ / n! whenever ‖p s‖ ≤ C for |s| ≤ |t|. The coefficient p need not be bounded on the whole line.

Existence on the whole line cannot be taken from TauCeti.timeDependentFlow, whose suspended field must be globally Lipschitz, nor from the Carathéodory solutions of TauCeti.exists_continuousOn_eq_forall_mem_Icc_eq_picard, which live on one compact interval; the series also supplies the explicit expansion. Uniqueness is Continuous.eq_of_hasDerivAt_clm_apply.

Applied in the opposite algebra, the same series solves the left equation Γ' t = p t * Γ t. For a path of bounded operators M on a Banach space this left series is the propagator of the time-dependent linear equation w' t = M t (w t): every solution is w t = Γ t (w 0).

If p takes skew-adjoint values in a star algebra, then Γ t is unitary. This is the mechanism producing the unitary cocycles which implement bounded perturbations of one-parameter automorphism groups of C⋆-algebras.

Main declarations

• TauCeti.dysonTerm: the n-fold iterated integral of the path.
• TauCeti.norm_dysonTerm_le: the factorial bound on the iterated integrals.
• TauCeti.dysonSeries: the sum of the iterated integrals.
• TauCeti.hasDerivAt_dysonSeries: the series solves Γ' t = Γ t * p t.
• TauCeti.eq_mul_dysonSeries: every solution of this equation is f 0 * Γ t.
• TauCeti.dysonSeries_mem_unitary: for skew-adjoint p the series is unitary.
• TauCeti.continuous_parametric_dysonSeries: the series of a jointly continuous family of paths depends continuously on the parameter, jointly with the time.
• TauCeti.dysonSeriesLeft: the Dyson series in the opposite algebra, solving Γ' t = p t * Γ t (TauCeti.hasDerivAt_dysonSeriesLeft), and factoring as Γ (t + d) = Γ t * Γ d for a path of period d (TauCeti.dysonSeriesLeft_add_of_periodic), hence Γ (n d) = Γ d ^ n (TauCeti.dysonSeriesLeft_natCast_mul_of_periodic).
• TauCeti.eq_dysonSeriesLeft_apply: for a path of bounded operators, every solution of the time-dependent linear equation w' t = M t (w t) is w t = dysonSeriesLeft M t (w 0).
• TauCeti.periodic_dysonSeriesLeft_apply_iff: for a periodic path of bounded operators, such a solution is periodic exactly when its initial value is fixed by the propagator over one period.
• TauCeti.apply_dysonSeriesLeft_apply_dysonSeriesLeft: the propagator of a continuous path that is skew for a continuous bilinear map B preserves B.
• TauCeti.contDiff_dysonSeriesLeft: the left series of a Cⁿ path is Cⁿ⁺¹.
• TauCeti.dysonSeries_neg_mul_dysonSeriesLeft, TauCeti.dysonSeriesLeft_mul_dysonSeries_neg: the Dyson series of -p is the inverse of the left Dyson series of p.
• TauCeti.eq_dysonSeriesLeft_apply_add_integral: variation of constants, every solution of w' t = M t (w t) + f t is w t = Γ t (w 0 + ∫₀ᵗ Γ(s)⁻¹ (f s) ds).

References

• Bratteli--Robinson, Operator Algebras and Quantum Statistical Mechanics 1, second edition, Theorem 3.1.33, for bounded perturbations and their Dyson expansions.
• Bratteli--Robinson, Operator Algebras and Quantum Statistical Mechanics 2, second edition, Section 5.4.1, for the unitary cocycles of perturbed C⋆-dynamics.

def TauCeti.dysonTerm {B : Type u_1} [NormedRing B] [NormedAlgebra ℝ B] (p : ℝ → B) : ℕ → ℝ → B

The n-th term of the Dyson series of p: dysonTerm p 0 t = 1 and dysonTerm p (n + 1) t = ∫ s in 0..t, dysonTerm p n s * p s. It is the iterated integral of p s₁ * ⋯ * p sₙ over the simplex 0 ≤ s₁ ≤ ⋯ ≤ sₙ ≤ t when t ≥ 0; when t < 0 it is (-1)ⁿ times the integral over the reversed simplex t ≤ sₙ ≤ ⋯ ≤ s₁ ≤ 0.

@[simp]

theorem TauCeti.dysonTerm_zero {B : Type u_1} [NormedRing B] [NormedAlgebra ℝ B] (p : ℝ → B) (t : ℝ) : dysonTerm p 0 t = 1

theorem TauCeti.dysonTerm_succ {B : Type u_1} [NormedRing B] [NormedAlgebra ℝ B] (p : ℝ → B) (n : ℕ) (t : ℝ) : dysonTerm p (n + 1) t = ∫ (s : ℝ) in 0..t, dysonTerm p n s * p s

The recursion defining the iterated integrals.

@[simp]

theorem TauCeti.dysonTerm_succ_zero {B : Type u_1} [NormedRing B] [NormedAlgebra ℝ B] (p : ℝ → B) (n : ℕ) : dysonTerm p (n + 1) 0 = 0

theorem TauCeti.continuous_dysonTerm {B : Type u_1} [NormedRing B] [NormedAlgebra ℝ B] {p : ℝ → B} (hp : Continuous p) (n : ℕ) : Continuous (dysonTerm p n)

The iterated integrals of a continuous path are continuous.

theorem TauCeti.continuous_parametric_dysonTerm {B : Type u_1} [NormedRing B] [NormedAlgebra ℝ B] {X : Type u_2} [TopologicalSpace X] {p : X → ℝ → B} (hp : Continuous (Function.uncurry p)) (n : ℕ) : Continuous fun (q : X × ℝ) => dysonTerm (p q.1) n q.2

The iterated integrals of a jointly continuous family of paths are jointly continuous in the parameter and the time.

theorem TauCeti.norm_dysonTerm_le {B : Type u_1} [NormedRing B] [NormedAlgebra ℝ B] {p : ℝ → B} {R C : ℝ} (hC : ∀ (s : ℝ), |s| ≤ R → ‖p s‖ ≤ C) (n : ℕ) {t : ℝ} (ht : |t| ≤ R) : ‖dysonTerm p n t‖ ≤ ‖1‖ * (C * |t|) ^ n / ↑n.factorial

The factorial bound on the iterated integrals: if ‖p s‖ ≤ C for |s| ≤ R, then ‖dysonTerm p n t‖ ≤ ‖1‖ * (C * |t|) ^ n / n! for |t| ≤ R.

theorem TauCeti.eq_of_hasDerivAt_mul {B : Type u_1} [NormedRing B] [NormedAlgebra ℝ B] {p : ℝ → B} (hp : Continuous p) {f g : ℝ → B} (hf : ∀ (t : ℝ), HasDerivAt f (f t * p t) t) (hg : ∀ (t : ℝ), HasDerivAt g (g t * p t) t) {t₀ : ℝ} (h : f t₀ = g t₀) : f = g

Uniqueness for the linear equation solved by the Dyson series: a solution of f' t = f t * p t is determined by its value at one time.

noncomputable def TauCeti.dysonSeries {B : Type u_1} [NormedRing B] [NormedAlgebra ℝ B] (p : ℝ → B) (t : ℝ) : B

The Dyson series, or time-ordered exponential, of p: the sum of the iterated integrals dysonTerm p n t. For continuous p it is the solution of Γ' t = Γ t * p t with Γ 0 = 1 (hasDerivAt_dysonSeries, eq_mul_dysonSeries).

@[simp]

theorem TauCeti.dysonSeries_zero {B : Type u_1} [NormedRing B] [NormedAlgebra ℝ B] (p : ℝ → B) : dysonSeries p 0 = 1

noncomputable def TauCeti.dysonSeriesLeft {B : Type u_1} [NormedRing B] [NormedAlgebra ℝ B] (p : ℝ → B) (t : ℝ) : B

The Dyson series of p for the left equation Γ' t = p t * Γ t: the Dyson series of p in the opposite algebra. For a path of bounded operators it is the propagator of the time-dependent linear equation w' t = p t (w t) (eq_dysonSeriesLeft_apply).

theorem TauCeti.op_dysonSeriesLeft {B : Type u_1} [NormedRing B] [NormedAlgebra ℝ B] (p : ℝ → B) (t : ℝ) : MulOpposite.op (dysonSeriesLeft p t) = dysonSeries (fun (s : ℝ) => MulOpposite.op (p s)) t

The left Dyson series of p is the Dyson series of p in the opposite algebra. This transfers the facts about dysonSeries to dysonSeriesLeft.

@[simp]

theorem TauCeti.dysonSeriesLeft_zero {B : Type u_1} [NormedRing B] [NormedAlgebra ℝ B] (p : ℝ → B) : dysonSeriesLeft p 0 = 1

theorem TauCeti.hasDerivAt_dysonTerm_succ {B : Type u_1} [NormedRing B] [NormedAlgebra ℝ B] {p : ℝ → B} [CompleteSpace B] (hp : Continuous p) (n : ℕ) (t : ℝ) : HasDerivAt (dysonTerm p (n + 1)) (dysonTerm p n t * p t) t

Each iterated integral is the primitive of the previous one multiplied by p.

theorem TauCeti.summable_dysonTerm {B : Type u_1} [NormedRing B] [NormedAlgebra ℝ B] {p : ℝ → B} [CompleteSpace B] (hp : Continuous p) (t : ℝ) : Summable fun (n : ℕ) => dysonTerm p n t

The iterated integrals are summable at every time.

theorem TauCeti.hasSum_dysonSeries {B : Type u_1} [NormedRing B] [NormedAlgebra ℝ B] {p : ℝ → B} [CompleteSpace B] (hp : Continuous p) (t : ℝ) : HasSum (fun (n : ℕ) => dysonTerm p n t) (dysonSeries p t)

The Dyson series converges in norm at every time.

theorem TauCeti.hasDerivAt_dysonSeries {B : Type u_1} [NormedRing B] [NormedAlgebra ℝ B] {p : ℝ → B} [CompleteSpace B] (hp : Continuous p) (t : ℝ) : HasDerivAt (dysonSeries p) (dysonSeries p t * p t) t

The Dyson series solves the linear equation Γ' t = Γ t * p t.

theorem TauCeti.continuous_dysonSeries {B : Type u_1} [NormedRing B] [NormedAlgebra ℝ B] {p : ℝ → B} [CompleteSpace B] (hp : Continuous p) : Continuous (dysonSeries p)

The Dyson series of a continuous path is continuous.

theorem TauCeti.continuous_parametric_dysonSeries {B : Type u_1} [NormedRing B] [NormedAlgebra ℝ B] [CompleteSpace B] {X : Type u_2} [TopologicalSpace X] {p : X → ℝ → B} (hp : Continuous (Function.uncurry p)) : Continuous fun (q : X × ℝ) => dysonSeries (p q.1) q.2

Continuous dependence on parameters. The Dyson series of a jointly continuous family of paths is jointly continuous in the parameter and the time.

theorem TauCeti.eq_mul_dysonSeries {B : Type u_1} [NormedRing B] [NormedAlgebra ℝ B] {p : ℝ → B} [CompleteSpace B] (hp : Continuous p) {f : ℝ → B} (hf : ∀ (t : ℝ), HasDerivAt f (f t * p t) t) (t : ℝ) : f t = f 0 * dysonSeries p t

Every solution of f' t = f t * p t is f 0 * dysonSeries p t.

theorem TauCeti.dysonSeries_mem_unitary {B : Type u_1} [NormedRing B] [NormedAlgebra ℝ B] {p : ℝ → B} [CompleteSpace B] [StarRing B] [ContinuousStar B] (hp : Continuous p) (hskew : ∀ (t : ℝ), star (p t) = -p t) (t : ℝ) : dysonSeries p t ∈ unitary B

The Dyson series of a skew-adjoint path is unitary.

The left equation and the propagator of a linear equation

theorem TauCeti.hasDerivAt_dysonSeriesLeft {B : Type u_1} [NormedRing B] [NormedAlgebra ℝ B] {p : ℝ → B} [CompleteSpace B] (hp : Continuous p) (t : ℝ) : HasDerivAt (dysonSeriesLeft p) (p t * dysonSeriesLeft p t) t

The left Dyson series solves the linear equation Γ' t = p t * Γ t.

theorem TauCeti.continuous_dysonSeriesLeft {B : Type u_1} [NormedRing B] [NormedAlgebra ℝ B] {p : ℝ → B} [CompleteSpace B] (hp : Continuous p) : Continuous (dysonSeriesLeft p)

The left Dyson series of a continuous path is continuous.

theorem TauCeti.continuous_parametric_dysonSeriesLeft {B : Type u_1} [NormedRing B] [NormedAlgebra ℝ B] [CompleteSpace B] {X : Type u_2} [TopologicalSpace X] {p : X → ℝ → B} (hp : Continuous (Function.uncurry p)) : Continuous fun (q : X × ℝ) => dysonSeriesLeft (p q.1) q.2

The left Dyson series of a jointly continuous family of paths is jointly continuous in the parameter and the time.

theorem TauCeti.eq_dysonSeriesLeft_mul {B : Type u_1} [NormedRing B] [NormedAlgebra ℝ B] {p : ℝ → B} [CompleteSpace B] (hp : Continuous p) {f : ℝ → B} (hf : ∀ (t : ℝ), HasDerivAt f (p t * f t) t) (t : ℝ) : f t = dysonSeriesLeft p t * f 0

Every solution of f' t = p t * f t is dysonSeriesLeft p t * f 0.

theorem TauCeti.dysonSeriesLeft_add_of_periodic {B : Type u_1} [NormedRing B] [NormedAlgebra ℝ B] {p : ℝ → B} [CompleteSpace B] (hp : Continuous p) {d : ℝ} (hper : Function.Periodic p d) (t : ℝ) : dysonSeriesLeft p (t + d) = dysonSeriesLeft p t * dysonSeriesLeft p d

For a periodic path, the left Dyson series over a translated period factors through the left Dyson series over one period: Γ (t + d) = Γ t * Γ d.

theorem TauCeti.dysonSeriesLeft_natCast_mul_of_periodic {B : Type u_1} [NormedRing B] [NormedAlgebra ℝ B] {p : ℝ → B} [CompleteSpace B] (hp : Continuous p) {d : ℝ} (hper : Function.Periodic p d) (n : ℕ) : dysonSeriesLeft p (↑n * d) = dysonSeriesLeft p d ^ n

For a periodic path, the left Dyson series over n periods is the n-th power of the left Dyson series over one period: Γ (n d) = Γ d ^ n. For a propagator this says that the return map of the n-fold iterated loop is the n-th power of the return map.

theorem TauCeti.dysonSeries_neg_mul_dysonSeriesLeft {B : Type u_1} [NormedRing B] [NormedAlgebra ℝ B] {p : ℝ → B} [CompleteSpace B] (hp : Continuous p) (t : ℝ) : dysonSeries (-p) t * dysonSeriesLeft p t = 1

The Dyson series of -p is a left inverse of the left Dyson series of p: dysonSeries (-p) t * dysonSeriesLeft p t = 1.

theorem TauCeti.dysonSeriesLeft_mul_dysonSeries_neg {B : Type u_1} [NormedRing B] [NormedAlgebra ℝ B] {p : ℝ → B} [CompleteSpace B] (hp : Continuous p) (t : ℝ) : dysonSeriesLeft p t * dysonSeries (-p) t = 1

The Dyson series of -p is a right inverse of the left Dyson series of p: dysonSeriesLeft p t * dysonSeries (-p) t = 1.

theorem TauCeti.isUnit_dysonSeriesLeft {B : Type u_1} [NormedRing B] [NormedAlgebra ℝ B] {p : ℝ → B} [CompleteSpace B] (hp : Continuous p) (t : ℝ) : IsUnit (dysonSeriesLeft p t)

The left Dyson series of a continuous path takes invertible values, with inverse the Dyson series of -p.

theorem TauCeti.contDiff_dysonSeriesLeft {B : Type u_1} [NormedRing B] [NormedAlgebra ℝ B] {p : ℝ → B} [CompleteSpace B] {n : ℕ} (hp : ContDiff ℝ (↑n) p) : ContDiff ℝ (↑n + 1) (dysonSeriesLeft p)

The left Dyson series of a Cⁿ path is Cⁿ⁺¹.

theorem TauCeti.eq_dysonSeriesLeft_apply {X : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {M : ℝ → X →L[ℝ] X} (hM : Continuous M) {w : ℝ → X} (hw : ∀ (t : ℝ), HasDerivAt w ((M t) (w t)) t) (t : ℝ) : w t = (dysonSeriesLeft M t) (w 0)

The propagator of a time-dependent linear equation. Every solution of w' t = M t (w t) for a continuous path M of bounded operators is w t = dysonSeriesLeft M t (w 0).

theorem TauCeti.hasDerivAt_dysonSeriesLeft_apply {X : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {M : ℝ → X →L[ℝ] X} (hM : Continuous M) (x : X) (t : ℝ) : HasDerivAt (fun (t : ℝ) => (dysonSeriesLeft M t) x) ((M t) ((dysonSeriesLeft M t) x)) t

The propagator applied to a fixed vector solves w' t = M t (w t).

theorem TauCeti.periodic_dysonSeriesLeft_apply_iff {X : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {M : ℝ → X →L[ℝ] X} (hM : Continuous M) {d : ℝ} (hper : Function.Periodic M d) (x : X) : Function.Periodic (fun (t : ℝ) => (dysonSeriesLeft M t) x) d ↔ (dysonSeriesLeft M d) x = x

For a continuous path M of period d, the solution t ↦ dysonSeriesLeft M t x of w' t = M t (w t) has period d exactly when x is fixed by the propagator over one period.

theorem TauCeti.apply_dysonSeriesLeft_apply_dysonSeriesLeft {X : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {M : ℝ → X →L[ℝ] X} (hM : Continuous M) {W : Type u_3} [NormedAddCommGroup W] [NormedSpace ℝ W] (B : X →L[ℝ] X →L[ℝ] W) (hskew : ∀ (r : ℝ) (u w : X), (B ((M r) u)) w + (B u) ((M r) w) = 0) (t : ℝ) (u w : X) : (B ((dysonSeriesLeft M t) u)) ((dysonSeriesLeft M t) w) = (B u) w

The propagator of a skew path preserves the bilinear form. If M is a continuous path of bounded operators with B (M r u) w + B u (M r w) = 0, then the propagator of w' t = M t (w t) preserves B.

theorem TauCeti.hasDerivAt_dysonSeriesLeft_apply_add_integral {X : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {M : ℝ → X →L[ℝ] X} (hM : Continuous M) {f : ℝ → X} (hf : Continuous f) (x : X) (t : ℝ) : HasDerivAt (fun (t : ℝ) => (dysonSeriesLeft M t) (x + ∫ (s : ℝ) in 0..t, (dysonSeries (-M) s) (f s))) ((M t) ((dysonSeriesLeft M t) (x + ∫ (s : ℝ) in 0..t, (dysonSeries (-M) s) (f s))) + f t) t

Variation of constants. For continuous M and f, the map w t = Ψ t (x + ∫₀ᵗ Ψ(s)⁻¹ (f s) ds), where Ψ = dysonSeriesLeft M and Ψ(s)⁻¹ = dysonSeries (-M) s, solves the inhomogeneous equation w' t = M t (w t) + f t.

theorem TauCeti.eq_dysonSeriesLeft_apply_add_integral {X : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {M : ℝ → X →L[ℝ] X} (hM : Continuous M) {f : ℝ → X} (hf : Continuous f) {w : ℝ → X} (hw : ∀ (t : ℝ), HasDerivAt w ((M t) (w t) + f t) t) (t : ℝ) : w t = (dysonSeriesLeft M t) (w 0 + ∫ (s : ℝ) in 0..t, (dysonSeries (-M) s) (f s))

Variation of constants. Every solution of w' t = M t (w t) + f t, for continuous M and f, is w t = Ψ t (w 0 + ∫₀ᵗ Ψ(s)⁻¹ (f s) ds), where Ψ = dysonSeriesLeft M and Ψ(s)⁻¹ = dysonSeries (-M) s.