MatrixPowerApproximation.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Stable powers of near-identity matrices

The telescoping estimate is the quantitative step needed to recover a one-parameter subgroup from the velocity of an actual subgroup curve. The number of factors grows, while their norms are bounded by a fixed exponential on the reciprocal scale.

lemma OAI.DukePrimeDegree.norm_pow_succ_sub_pow_succ_le line 23

theorem OAI.DukePrimeDegree.matrix_power_approximation line 49

Source documentation

The operator norm gives a dimension-free estimate for actual matrix powers; no entrywise bound is repeatedly amplified.

theorem matrix_power_approximation {n : ℕ}
    (A B : Matrix (Fin n) (Fin n) ℝ) (C : ℝ) (hC : 0 ≤ C) (N : ℕ)
    (hA : ‖A‖ ≤ Real.exp (C / (N + 1 : ℝ)))
    (hB : ‖B‖ ≤ Real.exp (C / (N + 1 : ℝ))) :
    ‖A ^ (N + 1) - B ^ (N + 1)‖ ≤ Real.exp C * ((N + 1 : ℝ) * ‖A - B‖) := by
…

theorem OAI.DukePrimeDegree.tendsto_matrix_power_difference_zero line 71

Source documentation

If the one-step error is little-o of the reciprocal number of factors, the products have the same limit.

theorem tendsto_matrix_power_difference_zero {n : ℕ}
    (A B : ℕ → Matrix (Fin n) (Fin n) ℝ) (C : ℝ) (hC : 0 ≤ C)
    (hA : ∀ᶠ N in atTop, ‖A N‖ ≤ Real.exp (C / (N + 1 : ℝ)))
    (hB : ∀ᶠ N in atTop, ‖B N‖ ≤ Real.exp (C / (N + 1 : ℝ)))
    (herr : Tendsto (fun N : ℕ => (N + 1 : ℝ) * ‖A N - B N‖) atTop (𝓝 0)) :
    Tendsto (fun N => ‖(A N) ^ (N + 1) - (B N) ^ (N + 1)‖) atTop (𝓝 0) := by
…