Matrix Square Root Difference Bound
ProvedFunctionalInequalities.Analysis.root_difference_bound_readableThis statement is a Sylvester-type estimate for two real matrices.
Let ι be a finite index type with decidable equality. Let S and T be matrices. Suppose S has quadratic floor a, T has quadratic floor b, and T is symmetric. Then
Here is the Frobenius norm represented by matrixEntries. The estimate does not require S and T to commute.
This bound is a reusable stability estimate for matrix square roots and inverse-square-root regularity.
Original Lean declaration header
Within namespace FunctionalInequalities.Analysis. Shown in its original module context. Proof omitted.
theorem root_difference_bound (S T : Matrix ι ι ℝ) {a b : ℝ}
(hS : QuadraticFloor S a) (hT : QuadraticFloor T b) (hSym : ∀ i j, T i j = T j i) :
(a + b) * ‖matrixEntries (S - T)‖ ≤ ‖matrixEntries (S * S - T * T)‖
Module navigation
Module: Analysis/Matrix/Positivity.
Previous: exists_quadraticFloor_of_posDef · Next: inverse_quadratic_young.
Source excerpt, lines 247–249 · Frozen source 408915f.
import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Matrix_Positivity
variable {ι κ : Type*} [Fintype ι] [Fintype κ]
variable [DecidableEq ι]
theorem FunctionalInequalities.Analysis.root_difference_bound_readable (S T : Matrix ι ι ℝ) {a b : ℝ}
(hS : QuadraticFloor S a) (hT : QuadraticFloor T b) (hSym : ∀ i j, T i j = T j i) :
(a + b) * ‖matrixEntries (S - T)‖ ≤ ‖matrixEntries (S * S - T * T)‖ := by sorry