Duhamel estimates for bounded generators

This file gives the variation identity and contraction bounds needed to compare exponentials of commuting bounded generators. The identity is oriented as exp (t B) - exp (t A), so its integrand acts on (B - A) x and the resulting estimate is immediately applicable to Yosida approximants.

theorem MarkovProcess.Semigroup.exp_sub_exp_apply_eq_integral {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (A B : E →L[ℝ] E) (hAB : Commute A B) (t : ℝ) (x : E) : (NormedSpace.exp (t • B)) x - (NormedSpace.exp (t • A)) x = ∫ (s : ℝ) in 0..t, (NormedSpace.exp ((t - s) • A)) ((NormedSpace.exp (s • B)) ((B - A) x))

Duhamel's identity for two commuting bounded generators, applied to a vector.

theorem MarkovProcess.Semigroup.norm_exp_sub_exp_apply_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (A B : E →L[ℝ] E) (hAB : Commute A B) {t : ℝ} (ht : 0 ≤ t) (hA : ∀ s ∈ Set.Icc 0 t, ‖NormedSpace.exp (s • A)‖ ≤ 1) (hB : ∀ s ∈ Set.Icc 0 t, ‖NormedSpace.exp (s • B)‖ ≤ 1) (x : E) : ‖(NormedSpace.exp (t • B)) x - (NormedSpace.exp (t • A)) x‖ ≤ t * ‖(B - A) x‖

Duhamel's contraction estimate for two commuting bounded generators.

theorem MarkovProcess.Semigroup.norm_exp_apply_sub_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (A : E →L[ℝ] E) {t : ℝ} (ht : 0 ≤ t) (hA : ∀ s ∈ Set.Icc 0 t, ‖NormedSpace.exp (s • A)‖ ≤ 1) (x : E) : ‖(NormedSpace.exp (t • A)) x - x‖ ≤ t * ‖A x‖

A contractive bounded exponential moves a vector by at most time times the norm of its generator applied to that vector.