Stat.Concentration.Matrix
Matrix concentration for random design moment matrices: iid entrywise deviation bounds, deterministic inverse perturbation, and high-probability control of the design inverse.
DesignInverse 1 core · 0 supporting Assembles deterministic inverse perturbation and iid union bounds into concentration for random design moment-matrix inverses. ★ designMatrix_inv_concentration
Matrix-inverse concentration for the random design moment matrix
Assembles deterministic inverse perturbation and iid union bounds into concentration for random design moment-matrix inverses.
This module assembles the two halves of the interior local-polynomial leverage rate
(M⁻¹)₀₀ = O(1/(Nh)) for the random design:
* Perturbation.designInv00_perturb — the deterministic transport: if the empirical moment
matrix M is entrywise within η of an invertible population matrix S whose inverse has
row sums bounded by c, with c·(p+1)·η ≤ 1/2, then M is invertible and
|(M⁻¹)₀₀ − (S⁻¹)₀₀| ≤ 2 c² (p+1) η.
* UnionBound.iid_sum_union_bound — the probabilistic half: each entry M_{jk}(ω) = ∑ᵢ g_{jk}(ωᵢ)
is an iid sum, so a union bound over the (p+1)² entries makes the entrywise-η good event
have probability ≥ 1 − ∑ Var/η².
The capstone designMatrix_inv_concentration combines them: the analytic failure event
(M singular, or (M⁻¹)₀₀ far from (S⁻¹)₀₀) has probability at most the union-bound tail.
Here the population matrix S = 𝔼[M] is supplied with its invertibility (IsUnit S.det, e.g. from
designMatrix_posDef) and an inverse-row-sum bound c; turning those into the explicit Θ(Nh)
density constants is the remaining kernel-change-of-variables step.
Matrix-inverse concentration of the random design moment matrix. Let g j k : Ω → ℝ be the per-entry design statistics, each square-integrable under μ, so the empirical moment matrix is M(ω) = fun j k => ∑ᵢ g j k (ωᵢ) and, given that the population matrix S equals N times its entrywise expectation, S j k = N·𝔼[g j k], suppose S is invertible with inverse row sums bounded by c ≥ 0, η is positive, and the scale satisfies c·(p+1)·η ≤ 1/2. Then the event on which M fails to be invertible or its leverage (M⁻¹)₀₀ is farther than 2 c² (p+1) η from (S⁻¹)₀₀ has probability at most the union-bound tail ∑_{j,k} N·Var[g j k]/η². This is the high-probability statement that the random design is non-degenerate with O(1/(Nh)) leverage on the good event.
Formal statement
Proof (Lean source)
IidSums 1 core · 2 supporting The interior nonparametric rates ((Nh)^{−1/2} variance, leverage O(1)) come from the behaviour of the random design moment sums ∑ᵢ K((Aᵢ−t)/h) (Aᵢ−t)ᵐ under an iid sample. ★ iid_sum_chebyshev
Concentration building blocks for the random design
The interior nonparametric rates ((Nh)^{−1/2} variance, leverage O(1)) come from the
behaviour of the random design moment sums ∑ᵢ K((Aᵢ−t)/h) (Aᵢ−t)ᵐ under an iid sample.
This file develops the elementary expectation/variance facts for such sums under the
product (iid) law Measure.pi, starting with linearity of expectation across the iid
coordinates:
𝔼[∑ᵢ g(Xᵢ)] = N · 𝔼[g].
These are the building blocks that turn the algebraic reductions (bias ≤ √(M₀₀(M⁻¹)₀₀),
variance ≤ σ² W (M⁻¹)₀₀) into rate statements via the design density.
Chebyshev concentration of an iid sum. Combining the iid expectation and variance laws with Chebyshev's inequality: for a fixed square-integrable statistic g and any positive threshold ε, the sum ∑ᵢ g(Xᵢ) over an iid sample of size N deviates from its mean N·𝔼[g] by at least ε with probability at most N·Var[g]/ε². For the design weight g = K((·−t)/h) this is the concentration of the total kernel weight M₀₀ around N·𝔼[K((A−t)/h)] = Θ(Nh).
Formal statement
Proof (Lean source)
2 supporting declarations (lemmas, instances)
-
integral_sum_pi_eqtheorem — Expectation of an iid sum. For an iid sample of size N drawn from a probability measure μ (modelled by the product measure Measure.pi), the expectation of the sum ∑ᵢ g(Xᵢ) of a fixed integrable statistic g equals N · 𝔼[g].hypothesesProof (Lean source)
theorem integral_sum_pi_eq {N : ℕ} {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω) [IsProbabilityMeasure μ] (g : Ω → ℝ) (hg : Integrable g μ) : ∫ ω, (∑ i : Fin N, g (ω i)) ∂(Measure.pi (fun _ : Fin N => μ)) = N * ∫ ω, g ω ∂μ := by let π : Measure (Fin N → Ω) := Measure.pi (fun _ : Fin N => μ) have hπ : ∀ i : Fin N, MeasurePreserving (Function.eval i) π μ := by intro i simpa [π] using measurePreserving_eval (fun _ : Fin N => μ) i change ∫ ω, (∑ i : Fin N, g (ω i)) ∂π = N * ∫ ω, g ω ∂μ calc ∫ ω, (∑ i : Fin N, g (ω i)) ∂π = ∑ i : Fin N, ∫ ω, g (ω i) ∂π := by rw [integral_finset_sum] intro i _ simpa [Function.comp_def] using (hπ i).integrable_comp_of_integrable hg _ = ∑ _i : Fin N, ∫ ω, g ω ∂μ := by apply Finset.sum_congr rfl intro i _ calc ∫ ω, g (ω i) ∂π = ∫ ω, g ω ∂Measure.map (Function.eval i) π := by refine (integral_map (hπ i).measurable.aemeasurable ?_).symm simpa [(hπ i).map_eq] using hg.aestronglyMeasurable _ = ∫ ω, g ω ∂μ := by rw [(hπ i).map_eq] _ = N * ∫ ω, g ω ∂μ := by simp [Finset.sum_const, nsmul_eq_mul] -
variance_sum_pi_eqtheorem — Variance of an iid sum. For an iid sample of size N from μ (the product measure Measure.pi), the variance of the sum ∑ᵢ g(Xᵢ) of a fixed L² statistic g equals N · Var[g] — the coordinate copies are independent, so cross-covariances vanish.hypothesesProof (Lean source)
theorem variance_sum_pi_eq {N : ℕ} {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω) [IsProbabilityMeasure μ] (g : Ω → ℝ) (hg : MemLp g 2 μ) : Var[fun ω => ∑ i : Fin N, g (ω i); Measure.pi (fun _ : Fin N => μ)] = N * Var[g; μ] := by rw [show (fun ω : Fin N → Ω => ∑ i : Fin N, g (ω i)) = (∑ i : Fin N, fun ω : Fin N → Ω => g (ω i)) by ext ω simp [Finset.sum_apply]] simpa [Finset.sum_const, nsmul_eq_mul] using (ProbabilityTheory.variance_sum_pi (μ := fun _ : Fin N => μ) (X := fun _ : Fin N => g) (fun _ : Fin N => hg))
InversePerturbation 1 core · 5 supporting Deterministic inverse-perturbation bounds that transport entrywise matrix deviations into control of a design inverse. ★ designInv00_perturb
Entrywise perturbation of the inverse design moment matrix
Deterministic inverse-perturbation bounds that transport entrywise matrix deviations into control of a design inverse.
The interior local-polynomial variance rate (M⁻¹)₀₀ = O(1/(Nh)) is obtained by transporting
an entrywise concentration bound on the random design moment matrix M (each entry close to
the corresponding entry of a fixed, invertible population matrix S) through the matrix
inverse. This file develops the deterministic perturbation step:
if every entry of M is within η of the corresponding entry of an invertible matrix S, and
the rows of S⁻¹ have absolute sums bounded by c, with c·(p+1)·η ≤ 1/2, then M is
invertible and
|(M⁻¹)₀₀ − (S⁻¹)₀₀| ≤ 2 c² (p+1) η.
The argument is the operator (ℓ∞-operator, i.e. max-row-sum) norm Neumann/resolvent bound:
M = S(1 − u) with u = S⁻¹(S − M), ‖u‖ ≤ ‖S⁻¹‖·‖S − M‖ ≤ 1/2, so 1 − u is a unit
(Units.oneSub) with ‖(1−u)⁻¹‖ ≤ (1−‖u‖)⁻¹ ≤ 2 (geometric series), hence M is a unit with
‖M⁻¹‖ ≤ 2‖S⁻¹‖, and the resolvent identity M⁻¹ − S⁻¹ = M⁻¹(S − M)S⁻¹
(norm_unitInv_sub_unitInv_le) gives ‖M⁻¹ − S⁻¹‖ ≤ 2‖S⁻¹‖²‖S − M‖. The entry bound follows
since each entry is dominated by the operator norm. The public statement carries only entrywise
hypotheses, so it composes with the iid Chebyshev union bound (for M close to 𝔼 M = S) and
the population positive-definiteness (designMatrix_posDef) without exposing the matrix norm.
The (0,0) specialization of the entrywise inverse perturbation bound. If S is invertible, every row of S⁻¹ has its absolute entries summing to at most c, every entry of M differs from the corresponding entry of S by at most η, and the product c · ((p+1) · η) is at most 1/2, then M is also invertible and its (0,0) inverse entry differs from S's by at most 2 · c² · ((p+1) · η).
Formal statement
Proof (Lean source)
5 supporting declarations (lemmas, instances)
-
completeSpace_matrix_linftyOptheorem — Completeness of finite matrices under the ℓ∞-operator norm follows from the coordinatewise function-space uniformity. Needed to invoke the Neumann/geometric-series unit API.Proof (Lean source)
theorem completeSpace_matrix_linftyOp {α β R : Type*} [Fintype α] [Fintype β] [NormedAddCommGroup R] [CompleteSpace R] : CompleteSpace (Matrix α β R) := inferInstanceAs (CompleteSpace (α → β → R)) -
linftyOp_abs_entry_letheorem — Each coefficient norm is dominated by the ℓ∞-operator (max-row-sum) norm.hypothesesconclusion‖A i j‖ ≤ ‖A‖Proof (Lean source)
theorem linftyOp_abs_entry_le {α β R : Type*} [Fintype α] [Fintype β] [NormedAddCommGroup R] (A : Matrix α β R) (i : α) (j : β) : ‖A i j‖ ≤ ‖A‖ := by rw [Matrix.linfty_opNorm_def] have hrow : ‖A i j‖₊ ≤ ∑ k, ‖A i k‖₊ := Finset.single_le_sum (s := univ) (f := fun k => ‖A i k‖₊) (fun _ _ => zero_le) (Finset.mem_univ j) have hsup : (∑ k, ‖A i k‖₊) ≤ Finset.univ.sup (fun i => ∑ k, ‖A i k‖₊) := Finset.le_sup (s := univ) (f := fun i => ∑ k, ‖A i k‖₊) (Finset.mem_univ i) exact_mod_cast le_trans hrow hsup -
linftyOp_norm_le_of_rowsumtheorem — A row-sum upper bound for the ℓ∞-operator norm: if every row's coefficient-norm sum is ≤ c, then ‖A‖ ≤ c.hypothesesα β R :c :ℝhc :0 ≤ ch :∀ i, (∑ j, ‖A i j‖) ≤ cconclusion‖A‖ ≤ cProof (Lean source)
theorem linftyOp_norm_le_of_rowsum {α β R : Type*} [Fintype α] [Fintype β] [NormedAddCommGroup R] {A : Matrix α β R} {c : ℝ} (hc : 0 ≤ c) (h : ∀ i, (∑ j, ‖A i j‖) ≤ c) : ‖A‖ ≤ c := by rw [Matrix.linfty_opNorm_def] have hsup : Finset.univ.sup (fun i => ∑ j, ‖A i j‖₊) ≤ c.toNNReal := by refine Finset.sup_le ?_ intro i _ exact NNReal.coe_le_coe.mp (by rw [NNReal.coe_sum, Real.coe_toNNReal c hc] simpa using h i) calc ↑(Finset.univ.sup fun i => ∑ j, ‖A i j‖₊) ≤ (c.toNNReal : ℝ) := NNReal.coe_le_coe.mpr hsup _ = c := Real.coe_toNNReal c hc -
linftyOp_norm_le_of_entrytheorem — The ℓ∞-operator norm of an entrywise-η-bounded rectangular matrix is at most its number of columns times η.hypothesesconclusion‖A‖ ≤ (q + 1 : ℕ) * ηProof (Lean source)
theorem linftyOp_norm_le_of_entry {q : ℕ} {A : Matrix (Fin (p + 1)) (Fin (q + 1)) ℝ} {η : ℝ} (h : ∀ i j, |A i j| ≤ η) : ‖A‖ ≤ (q + 1 : ℕ) * η := by have hη : 0 ≤ η := le_trans (abs_nonneg (A 0 0)) (h 0 0) apply linftyOp_norm_le_of_rowsum (mul_nonneg (by positivity) hη) intro i calc ∑ j, |A i j| ≤ ∑ _j : Fin (q + 1), η := Finset.sum_le_sum (fun j _ => h i j) _ = (q + 1 : ℕ) * η := by simp [Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul] -
designInv_perturbtheorem — Entrywise perturbation of an inverse entry. Let S be an invertible (p+1)×(p+1) real matrix whose inverse has rows with absolute sums bounded by c, and let M be a matrix all of whose entries are within η of S (|Mⱼₖ − Sⱼₖ| ≤ η). If c·(p+1)·η ≤ 1/2, then M is invertible and every selected pair of inverse entries satisfieshypotheseshS :IsUnit S.detη c :ℝhSrow :∀ i, (∑ j, |S⁻¹ i j|) ≤ chclose :∀ j k, |M j k - S j k| ≤ ηhsmall :c * ((p + 1 : ℕ) * η) ≤ 1 / 2i j :Fin (p + 1)conclusionIsUnit M.det ∧ |M⁻¹ i j - S⁻¹ i j| ≤ 2 * c ^ 2 * ((p + 1 : ℕ) * η)Proof (Lean source)
theorem designInv_perturb (S M : Matrix (Fin (p + 1)) (Fin (p + 1)) ℝ) (hS : IsUnit S.det) {η c : ℝ} (hSrow : ∀ i, (∑ j, |S⁻¹ i j|) ≤ c) (hclose : ∀ j k, |M j k - S j k| ≤ η) (hsmall : c * ((p + 1 : ℕ) * η) ≤ 1 / 2) {i j : Fin (p + 1)} : IsUnit M.det ∧ |M⁻¹ i j - S⁻¹ i j| ≤ 2 * c ^ 2 * ((p + 1 : ℕ) * η) := by haveI : CompleteSpace (Matrix (Fin (p + 1)) (Fin (p + 1)) ℝ) := completeSpace_matrix_linftyOp let R := Matrix (Fin (p + 1)) (Fin (p + 1)) ℝ have hSu : IsUnit S := (Matrix.isUnit_iff_isUnit_det S).mpr hS set Su : Rˣ := hSu.unit with hSu_def have hval : (↑Su : R) = S := by rw [hSu_def] exact hSu.unit_spec have hinv : (↑Su⁻¹ : R) = S⁻¹ := by rw [Matrix.coe_units_inv, hval] have hc : 0 ≤ c := le_trans (sum_nonneg fun _ _ => abs_nonneg _) (hSrow 0) have hSinv_norm : ‖(↑Su⁻¹ : R)‖ ≤ c := by rw [hinv] exact linftyOp_norm_le_of_rowsum hc hSrow have hMS_norm : ‖M - S‖ ≤ (p + 1 : ℕ) * η := linftyOp_norm_le_of_entry (by intro i j simpa [Matrix.sub_apply] using hclose i j) have hη : 0 ≤ η := le_trans (abs_nonneg (M 0 0 - S 0 0)) (hclose 0 0) have hdimη : 0 ≤ (p + 1 : ℕ) * η := mul_nonneg (by positivity) hη set u : R := (↑Su⁻¹ : R) * (S - M) with hu_def have hu_le : ‖u‖ ≤ c * ((p + 1 : ℕ) * η) := by calc ‖u‖ = ‖(↑Su⁻¹ : R) * (S - M)‖ := by rw [hu_def] _ ≤ ‖(↑Su⁻¹ : R)‖ * ‖S - M‖ := norm_mul_le _ _ _ = ‖(↑Su⁻¹ : R)‖ * ‖M - S‖ := by rw [norm_sub_rev S M] _ ≤ c * ((p + 1 : ℕ) * η) := by simpa [mul_comm] using mul_le_mul hMS_norm hSinv_norm (norm_nonneg _) hdimη have huhalf : ‖u‖ ≤ 1 / 2 := le_trans hu_le hsmall have hu1 : ‖u‖ < 1 := by have hunonneg : 0 ≤ ‖u‖ := norm_nonneg u nlinarith set v : Rˣ := Units.oneSub u hu1 with hv_def have hinvS : (↑Su⁻¹ : R) * S = 1 := by rw [← hval] exact_mod_cast Su.inv_mul have hSmulinv : S * (↑Su⁻¹ : R) = 1 := by rw [← hval] exact Su.mul_inv have hvval : (↑v : R) = (↑Su⁻¹ : R) * M := by rw [hv_def] change (1 : R) - u = (↑Su⁻¹ : R) * M rw [hu_def] calc (1 : R) - (↑Su⁻¹ : R) * (S - M) = (↑Su⁻¹ : R) * S - (↑Su⁻¹ : R) * (S - M) := by rw [hinvS] _ = (↑Su⁻¹ : R) * (S - (S - M)) := by rw [← mul_sub] _ = (↑Su⁻¹ : R) * M := by simp set Munit : Rˣ := Su * v with hM_def have hMval : (↑Munit : R) = M := by rw [hM_def] change ((↑Su : R) * (↑v : R)) = M rw [hval, hvval, ← mul_assoc, hSmulinv, one_mul] have hMunit : IsUnit M := hMval ▸ Munit.isUnit have hMdet : IsUnit M.det := (Matrix.isUnit_iff_isUnit_det M).mp hMunit have hMinv_eq : (↑Munit⁻¹ : R) = M⁻¹ := by rw [Matrix.coe_units_inv, hMval] have hvinv_norm : ‖(↑v⁻¹ : R)‖ ≤ (1 - ‖u‖)⁻¹ := by rw [hv_def] change ‖∑' n : ℕ, u ^ n‖ ≤ (1 - ‖u‖)⁻¹ have hgeo := tsum_geometric_le_of_norm_lt_one u hu1 rw [norm_one, sub_self, zero_add] at hgeo exact hgeo have hvinv2 : ‖(↑v⁻¹ : R)‖ ≤ 2 := by have hhalf_le : (1 / 2 : ℝ) ≤ 1 - ‖u‖ := by linarith have hhalf_pos : 0 < (1 / 2 : ℝ) := by norm_num have hinv_le : (1 - ‖u‖)⁻¹ ≤ 2 := by have hden_pos : 0 < 1 - ‖u‖ := by linarith calc (1 - ‖u‖)⁻¹ ≤ ((1 / 2 : ℝ)⁻¹) := (inv_le_inv₀ hden_pos hhalf_pos).mpr hhalf_le _ = 2 := by norm_num exact le_trans hvinv_norm hinv_le have hMunitinv_norm : ‖(↑Munit⁻¹ : R)‖ ≤ 2 * c := by calc ‖(↑Munit⁻¹ : R)‖ = ‖(↑v⁻¹ : R) * (↑Su⁻¹ : R)‖ := by rw [hM_def] rw [_root_.mul_inv_rev] rfl _ ≤ ‖(↑v⁻¹ : R)‖ * ‖(↑Su⁻¹ : R)‖ := norm_mul_le _ _ _ ≤ 2 * c := by exact mul_le_mul hvinv2 hSinv_norm (norm_nonneg _) (by norm_num) have hdiff_norm : ‖(↑Munit⁻¹ : R) - ↑Su⁻¹‖ ≤ 2 * c ^ 2 * ((p + 1 : ℕ) * η) := by have hres := norm_unitInv_sub_unitInv_le Munit Su calc ‖(↑Munit⁻¹ : R) - ↑Su⁻¹‖ ≤ ‖(↑Munit⁻¹ : R)‖ * ‖(↑Su⁻¹ : R)‖ * ‖(↑Munit : R) - ↑Su‖ := hres _ ≤ (2 * c) * c * ((p + 1 : ℕ) * η) := by have hdiff_mat : ‖(↑Munit : R) - ↑Su‖ ≤ (p + 1 : ℕ) * η := by simpa [hMval, hval] using hMS_norm have hAB : ‖(↑Munit⁻¹ : R)‖ * ‖(↑Su⁻¹ : R)‖ ≤ (2 * c) * c := mul_le_mul hMunitinv_norm hSinv_norm (norm_nonneg _) (by positivity) have hD_nonneg : 0 ≤ ‖(↑Munit : R) - ↑Su‖ := norm_nonneg _ have hC_nonneg : 0 ≤ (2 * c) * c := by positivity exact le_trans (mul_le_mul_of_nonneg_right hAB hD_nonneg) (mul_le_mul_of_nonneg_left hdiff_mat hC_nonneg) _ = 2 * c ^ 2 * ((p + 1 : ℕ) * η) := by ring refine ⟨hMdet, ?_⟩ calc |M⁻¹ i j - S⁻¹ i j| = |(((↑Munit⁻¹ : R) - ↑Su⁻¹) i j)| := by rw [← hMinv_eq, ← hinv, Matrix.sub_apply] _ ≤ ‖(↑Munit⁻¹ : R) - ↑Su⁻¹‖ := linftyOp_abs_entry_le ((↑Munit⁻¹ : R) - ↑Su⁻¹) i j _ ≤ 2 * c ^ 2 * ((p + 1 : ℕ) * η) := hdiff_norm
InverseUnionBound 1 core · 0 supporting The random design moment matrix has entries M_{jk}(ω) = ∑ᵢ h_{jk}(ωᵢ) with h_{jk}(a) = K((a−t)/h)·(a−t)^{j+k} — each entry is an iid sum, so it concentrates around its mean N·𝔼[h_{jk}] by iid_sum_chebyshev. ★ iid_sum_union_bound
Union bound for entrywise design-matrix concentration
The random design moment matrix has entries M_{jk}(ω) = ∑ᵢ h_{jk}(ωᵢ) with
h_{jk}(a) = K((a−t)/h)·(a−t)^{j+k} — each entry is an iid sum, so it concentrates around its
mean N·𝔼[h_{jk}] by iid_sum_chebyshev. To control the whole (p+1)²-entry matrix at once
(the "good event" on which the inverse perturbation bound applies) we union-bound over the
finite index set: the probability that some coordinate sum deviates from its mean by at least
η is at most the sum of the per-coordinate Chebyshev bounds.
This is the probabilistic half of the matrix-inverse concentration: combined with the
deterministic entrywise perturbation bound (designInv00_perturb), it shows that on an event of
probability ≥ 1 − ∑ Var/η² the empirical moment matrix is invertible with controlled leverage.
Union bound for iid coordinate sums. For a finite family g : ι → Ω → ℝ such that each g a is square-integrable under μ, evaluated on an iid sample of size N drawn from the product law Measure.pi, and for any positive deviation threshold η, the probability that some index a has its sample sum ∑ᵢ g a (ωᵢ) deviate from its mean N·𝔼[g a] by at least η is bounded by the sum of the per-index Chebyshev bounds N·Var[g a]/η².
Formal statement
Proof (Lean source)
Resolvent 1 core · 0 supporting The interior local-polynomial variance rate (M⁻¹)₀₀ = O(1/(Nh)) is obtained by concentrating the random design moment matrix M (entrywise, via the iid Chebyshev bound) around a fixed positive-definite population matrix a ★ norm_unitInv_sub_unitInv_le
Quantitative inverse perturbation bound
The interior local-polynomial variance rate (M⁻¹)₀₀ = O(1/(Nh)) is obtained by concentrating
the random design moment matrix M (entrywise, via the iid Chebyshev bound) around a fixed
positive-definite population matrix and transporting the bound through the matrix inverse. The
quantitative tool for that transport is the resolvent (first-resolvent) inequality
‖a⁻¹ − b⁻¹‖ ≤ ‖a⁻¹‖ · ‖b⁻¹‖ · ‖a − b‖,
valid for any two units a, b of a normed ring (a⁻¹ − b⁻¹ = a⁻¹ (b − a) b⁻¹ and
submultiplicativity of the norm). This is the explicit-constant companion to Mathlib's
asymptotic inverse_continuousAt / inverse_add_norm_diff_first_order.
Resolvent inequality. For a seminormed ring R and units a and b of R, the norm of the difference of their inverses is bounded above by the product of the norms of the two inverses and the norm of their difference.