Exponential limits and the Lie–Trotter formula

TheoremTelescoping estimate for differences of powers in a normed ring#✓fully proved

Telescoping estimate for powers in a normed ring with ‖1‖ = 1: ‖a ^ m - b ^ m‖ ≤ m ‖a - b‖ max(‖a‖, ‖b‖) ^ (m - 1).

theorem norm_pow_sub_pow_le (a b : 𝔸) (m : ℕ) :
    ‖a ^ m - b ^ m‖ ≤ m * ‖a - b‖ * max ‖a‖ ‖b‖ ^ (m - 1)

Used by 1

Used byCompound-interest limit in a Banach algebra

TheoremCompound-interest limit in a Banach algebra#✓fully proved

If Y M → X and m M / M → t, then (1 + M⁻¹ • Y M) ^ m M → exp (t • X) as M → ∞.

theorem tendsto_one_add_inv_smul_pow {Y : ℕ → 𝔸} {X : 𝔸} (hY : Tendsto Y atTop (𝓝 X))
    {m : ℕ → ℕ} {t : ℝ} (hm : Tendsto (fun M : ℕ => (m M : ℝ) / M) atTop (𝓝 t)) :
    Tendsto (fun M : ℕ => (1 + (M : ℝ)⁻¹ • Y M) ^ m M) atTop (𝓝 (exp (t • X)))

Uses 1 · Used by 1

Proof usesTelescoping estimate for differences of powers in a normed ring

Used byKingman's theorem for the lineage count

TheoremNorm of the exponential is bounded by the exponential of the norm#✓fully proved

The exponential is bounded by the real exponential of the norm.

theorem norm_exp_le_exp_norm {𝔸 : Type*} [NormedRing 𝔸] [NormedAlgebra ℚ 𝔸]
    [NormOneClass 𝔸] (x : 𝔸) : ‖NormedSpace.exp x‖ ≤ Real.exp ‖x‖

Used by 2

Used byOne-step Trotter estimate · Trotter product formula

TheoremFirst-order Taylor remainder bound for the exponential#✓fully proved

The Taylor remainder of exp at order one.

theorem norm_exp_sub_one_sub_id_le (x : 𝔸) :
    ‖NormedSpace.exp x - 1 - x‖ ≤ ‖x‖ ^ 2 * Real.exp ‖x‖

Used by 1

Used byOne-step Trotter estimate

TheoremOne-step Trotter estimate#✓fully proved

The one-step Trotter estimate: exp x * exp y differs from exp (x + y) by at most a quadratic expression in ‖x‖ and ‖y‖.

theorem norm_exp_mul_exp_sub_exp_add_le (x y : 𝔸) :
    ‖NormedSpace.exp x * NormedSpace.exp y - NormedSpace.exp (x + y)‖ ≤
      ‖x‖ * ‖y‖ + ‖x‖ ^ 2 * Real.exp ‖x‖ * Real.exp ‖y‖ +
        (1 + ‖x‖) * (‖y‖ ^ 2 * Real.exp ‖y‖) +
        (‖x‖ + ‖y‖) ^ 2 * Real.exp (‖x‖ + ‖y‖)

Uses 2 · Used by 1

Proof usesNorm of the exponential is bounded by the exponential of the norm · First-order Taylor remainder bound for the exponential

Used byTrotter product formula

TheoremLinear bound on differences of powers for the Trotter formula#✓fully proved

Powers differ at most linearly in the difference of the bases. The 1 in the maximum is needed: without it the bound fails when the norms are < 1.

theorem norm_pow_sub_pow_le {𝔸 : Type*} [NormedRing 𝔸] [NormOneClass 𝔸]
    (X Y : 𝔸) (n : ℕ) :
    ‖X ^ n - Y ^ n‖ ≤ (n : ℝ) * ‖X - Y‖ * (max (max ‖X‖ ‖Y‖) 1) ^ n

Used by 1

Used byTrotter product formula

TheoremTrotter product formula#✓fully proved

The Trotter product formula for bounded elements of a complete normed algebra: (exp (a / n) * exp (b / n)) ^ n → exp (a + b) in norm.

theorem tendsto_trotter_product (a b : 𝔸) :
    Tendsto (fun n : ℕ =>
      (NormedSpace.exp ((n : ℚ)⁻¹ • a) * NormedSpace.exp ((n : ℚ)⁻¹ • b)) ^ n)
      atTop (nhds (NormedSpace.exp (a + b)))

Uses 3

Proof usesNorm of the exponential is bounded by the exponential of the norm · One-step Trotter estimate · Linear bound on differences of powers for the Trotter formula

TheoremTrotter product formula for commuting elements#✓fully proved

If a and b commute, the Trotter approximants are exactly exp (a + b) for every positive n.

theorem trotter_product_of_commute {𝔸 : Type*} [NormedRing 𝔸] [NormedAlgebra ℚ 𝔸]
    [CompleteSpace 𝔸] {a b : 𝔸} (h : Commute a b) {n : ℕ} (hn : 0 < n) :
    (NormedSpace.exp ((n : ℚ)⁻¹ • a) * NormedSpace.exp ((n : ℚ)⁻¹ • b)) ^ n =
      NormedSpace.exp (a + b)

8 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.