FARMSAcceptedProposition · Statement with omitted proof
Positive semidefinite inverse perturbation inequality
A positive semidefinite perturbation bounds the change from the identity to its shifted inverse.
Halko, Martinsson & Tropp ↗
Source label: prop:perturb-inv
Formal statement. The assumptions and conclusion are explicit; the theorem proof is omitted (sorry).
01 / MATHEMATICAL STATEMENT
Meaning & conditions
Mathematical summary
A positive semidefinite perturbation bounds the change from the identity to its shifted inverse.
Assumptions & context
- M is a square positive semidefinite matrix over ℝ or ℂ.
Source
Halko, Martinsson & Tropp. Finding structure with randomness.
Source label: prop:perturb-inv
02 / LEAN REPRESENTATION
Formal statement
Statement with omitted proof. Expand the complete file below to read imports, local definitions and surrounding context.
theorem perturb_inv {𝕜 : Type*} [RCLike 𝕜] {n : ℕ}
(M : Matrix (Fin n) (Fin n) 𝕜) (hM : PsdLe 0 M) :
PsdLe (1 - (1 + M)⁻¹) M := by
sorry
Complete Lean file and local definitions
import RNLAPhaseB.B3Base
import RNLAPhaseB.Complexity
open MeasureTheory
open scoped Matrix
open scoped Matrix.Norms.L2Operator
open scoped BigOperators
open scoped ENNReal
open scoped ComplexOrder
namespace RNLAPhaseB.HMTPerturbInv
/-- The positive-semidefinite (Loewner) order `A ≼ B` (source notation `\psdle`):
`B - A` is positive semidefinite. `0 ≼ M` (source `M \psdge 0`) means `M` is psd. -/
def PsdLe {𝕜 : Type*} [RCLike 𝕜] {n : ℕ}
(A B : Matrix (Fin n) (Fin n) 𝕜) : Prop :=
(B - A).PosSemidef
/-- HMT 2011, Proposition `prop:perturb-inv`: if `M ≽ 0` then `I - (I + M)⁻¹ ≼ M`.
The field is either ℝ or ℂ, covered uniformly by `RCLike 𝕜`. -/
theorem perturb_inv {𝕜 : Type*} [RCLike 𝕜] {n : ℕ}
(M : Matrix (Fin n) (Fin n) 𝕜) (hM : PsdLe 0 M) :
PsdLe (1 - (1 + M)⁻¹) M := by
sorry
end RNLAPhaseB.HMTPerturbInv
How to read the formalization
- The relation is Loewner order, represented by positive semidefiniteness of a matrix difference.