FARMSAcceptedProposition · Statement with omitted proof
Monotonicity under enlargement of a projection space
A larger projection space increases the captured norm and decreases the residual norm.
Halko, Martinsson & Tropp ↗
Source label: prop:proj-range
Formal statement. The assumptions and conclusion are explicit; the theorem proof is omitted (sorry).
01 / MATHEMATICAL STATEMENT
Meaning & conditions
Mathematical summary
A larger projection space increases the captured norm and decreases the residual norm.
Assumptions & context
- The column space of N is contained in that of M; A has compatible dimensions.
Source
Halko, Martinsson & Tropp. Finding structure with randomness.
Source label: prop:proj-range
02 / LEAN REPRESENTATION
Formal statement
Statement with omitted proof. Expand the complete file below to read imports, local definitions and surrounding context.
theorem proj_range_norm_monotone
{𝕜 : Type*} [RCLike 𝕜] {m k l : ℕ}
(M : Matrix (Fin m) (Fin k) 𝕜) (N : Matrix (Fin m) (Fin l) 𝕜)
(hNM : matrixColumnSpace N ≤ matrixColumnSpace M) :
∀ {n : ℕ} (A : Matrix (Fin m) (Fin n) 𝕜),
‖orthogonalProjector N * A‖ ≤ ‖orthogonalProjector M * A‖ ∧
‖(1 - orthogonalProjector M) * A‖ ≤ ‖(1 - orthogonalProjector N) * A‖ := 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
namespace RNLAPhaseB.HMT2011PropProjRange
/-- HMT 2011, Proposition (prop:proj-range).
Suppose `range(N) ⊂ range(M)`. Then, for each matrix `A`, it holds that
`‖P_N A‖ ≤ ‖P_M A‖` and `‖(I - P_M) A‖ ≤ ‖(I - P_N) A‖`.
Here `P_M` is the audited orthogonal projector onto the column space of `M`
(`orthogonalProjector M`). `‖·‖` is the ℓ₂ operator (spectral) norm, the
scoped `Matrix.Norms.L2Operator` instance. `⊂` is non-strict inclusion of
column spaces. The scalar field is any `RCLike` field, covering both the real
and the complex case. `M`, `N` and `A` share the ambient row dimension `m`;
their column counts are arbitrary. -/
theorem proj_range_norm_monotone
{𝕜 : Type*} [RCLike 𝕜] {m k l : ℕ}
(M : Matrix (Fin m) (Fin k) 𝕜) (N : Matrix (Fin m) (Fin l) 𝕜)
(hNM : matrixColumnSpace N ≤ matrixColumnSpace M) :
∀ {n : ℕ} (A : Matrix (Fin m) (Fin n) 𝕜),
‖orthogonalProjector N * A‖ ≤ ‖orthogonalProjector M * A‖ ∧
‖(1 - orthogonalProjector M) * A‖ ≤ ‖(1 - orthogonalProjector N) * A‖ := by
sorry
end RNLAPhaseB.HMT2011PropProjRange
How to read the formalization
- Both conclusions use the spectral operator norm and actual orthogonal projectors.