From 74a0c03908031f416ce6b2cd1816bb78fea5cff3 Mon Sep 17 00:00:00 2001 From: HighDimProb Dev Date: Sat, 13 Jun 2026 07:38:20 +0000 Subject: [PATCH 1/2] Expose PSD nullspace bridge for covariance prerequisites This closes the narrow deterministic PSD kernel prerequisite by routing HighDimProb's explicit quadratic-form vocabulary through Mathlib's positive-semidefinite kernel theorem, then documenting the remaining boundary. Constraint: local/Workflow.md requires theory citations, review gates, docs updates, and full build/test/judge validation before PR. Rejected: prove expectation contraction in this branch | it is the next separate concept cluster and needs its own API audit. Confidence: high Scope-risk: narrow Directive: Keep this branch limited to PSD nullspace converse and examples-local adapters; do not fold in Matrix Bernstein tail or expectation-contraction work. Tested: lake build; lake test; lake build HighDimProbJudge; python scripts/judge_policy_check.py; git diff --check; forbidden-token/conflict-marker/comment-source review. Not-tested: External GitHub CI has not run before PR creation. --- .../RandomMatrix/KernelNullspaceUsage.lean | 87 +++++++++++++++++-- HighDimProb/RandomMatrix/Spectral.lean | 61 +++++++++++++ .../RandomMatrix/SpectralUse.lean | 38 ++++++++ HighDimProbTest/ExamplesAPI.lean | 30 +++++++ HighDimProbTest/RandomMatrixSpectralAPI.lean | 29 +++++++ docs/AbstractionLog.md | 22 ++++- docs/BookProgress.md | 30 +++++-- docs/MatrixBernsteinProofPlan.md | 10 ++- docs/MatrixConcentrationPlan.md | 10 ++- docs/RandomMatrixAPI.md | 17 +++- docs/Status.md | 35 +++++--- docs/TODO.md | 18 ++-- docs/TermMap.md | 5 +- docs/TheoremAtlas.md | 41 ++++++--- 14 files changed, 379 insertions(+), 54 deletions(-) diff --git a/HighDimProb/Examples/RandomMatrix/KernelNullspaceUsage.lean b/HighDimProb/Examples/RandomMatrix/KernelNullspaceUsage.lean index 3835c32..00a5d43 100644 --- a/HighDimProb/Examples/RandomMatrix/KernelNullspaceUsage.lean +++ b/HighDimProb/Examples/RandomMatrix/KernelNullspaceUsage.lean @@ -2,15 +2,15 @@ import HighDimProb.Examples.RandomMatrix.RankOnePSDUsage import HighDimProb.Examples.RandomMatrix.NTKGramDecompositionUsage import HighDimProb.Examples.RandomMatrix.RandomFeatureKernelUsage import HighDimProb.Examples.RandomMatrix.GradientCovarianceUsage +import HighDimProb.RandomMatrix.Spectral /-! # Kernel nullspace usage example This examples-only file introduces nullspace and invisible-direction vocabulary for kernel, NTK Gram, random-feature, and gradient covariance matrices. It -keeps the vocabulary deterministic and conservative. Hard PSD converses such as -`x^T A x = 0` implying `A x = 0` are exposed as local adapter assumptions -instead of being promoted to core. +keeps the vocabulary deterministic and conservative. The PSD nullspace converse +is supplied by the core bridge in `HighDimProb.RandomMatrix.Spectral`. -/ namespace HighDimProb.Examples.RandomMatrix.KernelNullspaceUsage @@ -72,6 +72,20 @@ theorem matrixQuadraticForm_eq_sum_mul_matrixAction {n : Nat} intro j _hj ring +/-- The examples-local `matrixAction` is Mathlib's matrix-vector +multiplication. + +Formula reference: the PSD nullspace converse is stated for the usual matrix +action `A x`; see +https://math.stackexchange.com/questions/3918031/prove-that-if-xtax-0-rightarrow-ax-0 . +-/ +theorem matrixAction_eq_mulVec {n : Nat} + (A : Matrix (Fin (n + 1)) (Fin (n + 1)) Real) + (x : Fin (n + 1) -> Real) : + matrixAction A x = Matrix.mulVec A x := by + ext i + simp [matrixAction, Matrix.mulVec, dotProduct] + /-- If `A x = 0`, then `x^T A x = 0`. -/ theorem quadraticNullDirection_of_invisible {n : Nat} {A : Matrix (Fin (n + 1)) (Fin (n + 1)) Real} @@ -93,6 +107,59 @@ theorem randomQuadraticNullDirection_of_invisible {Omega : Type*} intro omega exact quadraticNullDirection_of_invisible (h omega) +/-- PSD nullspace converse for the examples-local invisible-direction +vocabulary, using Mathlib `Matrix.PosSemidef`. + +Formula reference: a real symmetric positive semidefinite matrix with +`x^T A x = 0` sends `x` to zero; see +https://en.wikipedia.org/wiki/Definite_matrix#Square_root . +-/ +theorem invisible_of_quadraticNull_of_posSemidef {n : Nat} + {A : Matrix (Fin (n + 1)) (Fin (n + 1)) Real} + {x : Fin (n + 1) -> Real} + (hPSD : A.PosSemidef) + (hNull : KernelQuadraticNullDirection A x) : + KernelInvisibleDirection A x := by + unfold KernelQuadraticNullDirection at hNull + unfold KernelInvisibleDirection + rw [matrixAction_eq_mulVec] + exact matrix_mulVec_eq_zero_of_posSemidef_quadraticForm_eq_zero hPSD hNull + +/-- PSD nullspace converse for the examples-local vocabulary, using +HighDimProb's explicit `IsPSDMatrix` predicate. -/ +theorem invisible_of_quadraticNull_of_psd {n : Nat} + {A : Matrix (Fin (n + 1)) (Fin (n + 1)) Real} + {x : Fin (n + 1) -> Real} + (hPSD : IsPSDMatrix A) + (hNull : KernelQuadraticNullDirection A x) : + KernelInvisibleDirection A x := by + unfold KernelQuadraticNullDirection at hNull + unfold KernelInvisibleDirection + rw [matrixAction_eq_mulVec] + exact matrix_mulVec_eq_zero_of_isPSDMatrix_quadraticForm_eq_zero hPSD hNull + +/-- Pointwise random version of the Mathlib-PSD nullspace converse. -/ +theorem randomInvisible_of_quadraticNull_of_posSemidef {Omega : Type*} + [MeasurableSpace Omega] {n : Nat} + {A : RandomMatrix Omega (n + 1) (n + 1)} + {x : Fin (n + 1) -> Real} + (hPSD : forall omega, Matrix.PosSemidef (A omega)) + (hNull : RandomKernelQuadraticNullDirection A x) : + RandomKernelInvisibleDirection A x := by + intro omega + exact invisible_of_quadraticNull_of_posSemidef (hPSD omega) (hNull omega) + +/-- Pointwise random version of the explicit-PSD nullspace converse. -/ +theorem randomInvisible_of_quadraticNull_of_psd {Omega : Type*} + [MeasurableSpace Omega] {P : MeasureTheory.Measure Omega} {n : Nat} + {A : RandomMatrix Omega (n + 1) (n + 1)} + {x : Fin (n + 1) -> Real} + (hPSD : RandomPSDMatrix P A) + (hNull : RandomKernelQuadraticNullDirection A x) : + RandomKernelInvisibleDirection A x := by + intro omega + exact invisible_of_quadraticNull_of_psd (hPSD omega) (hNull omega) + /-- A direction orthogonal to a feature vector. -/ def OrthogonalToFeature {n : Nat} (v : RankOneVector n) (x : Fin (n + 1) -> Real) : Prop := @@ -148,17 +215,25 @@ theorem gradientOuter_invisible_of_orthogonal {n : Nat} simpa [gradientOuter_eq_rankOneOuter] using rankOneOuter_invisible_of_orthogonal (v := g) (x := x) h -/-- Example-local adapter for the hard PSD converse. +/-- Example-local adapter for the PSD converse. For PSD matrices the mathematical statement is that `x^T A x = 0` should -force `A x = 0`. The current example layer records it as a named assumption -waiting for future core support instead of proving a full PSD nullspace theory. -/ +force `A x = 0`. This predicate is kept as compatibility vocabulary for older +examples; `psdQuadraticNullImpliesInvisible_of_core` below supplies it from the +core PSD nullspace bridge. -/ def PSDQuadraticNullImpliesInvisible {n : Nat} (A : Matrix (Fin (n + 1)) (Fin (n + 1)) Real) : Prop := IsPSDMatrix A -> forall x : Fin (n + 1) -> Real, KernelQuadraticNullDirection A x -> KernelInvisibleDirection A x +/-- The core PSD nullspace bridge supplies the examples-local adapter. -/ +theorem psdQuadraticNullImpliesInvisible_of_core {n : Nat} + (A : Matrix (Fin (n + 1)) (Fin (n + 1)) Real) : + PSDQuadraticNullImpliesInvisible A := by + intro hPSD x hNull + exact invisible_of_quadraticNull_of_psd hPSD hNull + /-- Use the local PSD-nullspace adapter to turn a quadratic-null direction into an invisible direction. -/ theorem invisible_of_quadraticNull_of_psd_adapter {n : Nat} diff --git a/HighDimProb/RandomMatrix/Spectral.lean b/HighDimProb/RandomMatrix/Spectral.lean index 18e56b6..6d4cbd9 100644 --- a/HighDimProb/RandomMatrix/Spectral.lean +++ b/HighDimProb/RandomMatrix/Spectral.lean @@ -380,6 +380,67 @@ theorem matrixQuadraticForm_nonneg_of_posSemidef {n : Nat} simpa [matrixQuadraticForm, dotProduct, Matrix.mulVec, Finset.mul_sum, Finset.sum_mul, mul_assoc] using h +/-- HighDimProb's explicit PSD predicate gives Mathlib positive +semidefiniteness. + +Formula reference: positive semidefinite real matrices are characterized by a +nonnegative quadratic form; see https://en.wikipedia.org/wiki/Definite_matrix . +This bridge keeps the explicit HighDimProb assumptions visible while exposing +Mathlib's `Matrix.PosSemidef` API. -/ +theorem posSemidef_of_isPSDMatrix {n : Nat} + {A : Matrix (Fin n) (Fin n) Real} (hA : IsPSDMatrix A) : + A.PosSemidef := by + apply Matrix.PosSemidef.of_dotProduct_mulVec_nonneg + · apply Matrix.IsHermitian.ext + intro i j + simpa using Matrix.IsSymm.apply hA.1 i j + · intro x + have hx := hA.2 x + simpa [matrixQuadraticForm, dotProduct, Matrix.mulVec, + Finset.mul_sum, Finset.sum_mul, mul_assoc] using hx + +/-- PSD nullspace converse in HighDimProb's explicit quadratic-form vocabulary. + +Formula reference: for a positive semidefinite matrix, a zero quadratic form +forces the vector into the kernel; one proof uses the PSD square root, see +https://en.wikipedia.org/wiki/Definite_matrix#Square_root . This theorem is a +thin wrapper over Mathlib's `Matrix.PosSemidef.dotProduct_mulVec_zero_iff`. -/ +theorem matrixQuadraticForm_eq_zero_iff_mulVec_eq_zero_of_posSemidef {n : Nat} + {A : Matrix (Fin n) (Fin n) Real} (hA : A.PosSemidef) + (x : Fin n -> Real) : + matrixQuadraticForm A x = 0 <-> Matrix.mulVec A x = 0 := by + have h := hA.dotProduct_mulVec_zero_iff x + simpa [matrixQuadraticForm, dotProduct, Matrix.mulVec, + Finset.mul_sum, Finset.sum_mul, mul_assoc] using h + +/-- One-way PSD nullspace converse from a zero HighDimProb quadratic form. -/ +theorem matrix_mulVec_eq_zero_of_posSemidef_quadraticForm_eq_zero {n : Nat} + {A : Matrix (Fin n) (Fin n) Real} (hA : A.PosSemidef) + {x : Fin n -> Real} (hx : matrixQuadraticForm A x = 0) : + Matrix.mulVec A x = 0 := + (matrixQuadraticForm_eq_zero_iff_mulVec_eq_zero_of_posSemidef hA x).mp hx + +/-- Explicit-PSD version of the PSD nullspace iff. + +Formula reference: the statement is the usual PSD nullspace converse for +symmetric positive semidefinite real matrices; see +https://math.stackexchange.com/questions/3918031/prove-that-if-xtax-0-rightarrow-ax-0 . +-/ +theorem matrixQuadraticForm_eq_zero_iff_mulVec_eq_zero_of_isPSDMatrix {n : Nat} + {A : Matrix (Fin n) (Fin n) Real} (hA : IsPSDMatrix A) + (x : Fin n -> Real) : + matrixQuadraticForm A x = 0 <-> Matrix.mulVec A x = 0 := + matrixQuadraticForm_eq_zero_iff_mulVec_eq_zero_of_posSemidef + (posSemidef_of_isPSDMatrix hA) x + +/-- One-way explicit-PSD nullspace converse from a zero HighDimProb quadratic +form. -/ +theorem matrix_mulVec_eq_zero_of_isPSDMatrix_quadraticForm_eq_zero {n : Nat} + {A : Matrix (Fin n) (Fin n) Real} (hA : IsPSDMatrix A) + {x : Fin n -> Real} (hx : matrixQuadraticForm A x = 0) : + Matrix.mulVec A x = 0 := + (matrixQuadraticForm_eq_zero_iff_mulVec_eq_zero_of_isPSDMatrix hA x).mp hx + /-- Scalar-matrix quadratic form over an explicit unit vector. This is the small algebraic bridge needed to turn a Loewner-order upper bound diff --git a/HighDimProbJudge/RandomMatrix/SpectralUse.lean b/HighDimProbJudge/RandomMatrix/SpectralUse.lean index f0878a0..a903881 100644 --- a/HighDimProbJudge/RandomMatrix/SpectralUse.lean +++ b/HighDimProbJudge/RandomMatrix/SpectralUse.lean @@ -31,6 +31,11 @@ import HighDimProb.RandomMatrix #check HighDimProb.spectralUpperBound_of_lambdaMaxPSDUpperBound #check HighDimProb.spectralUpperBound_of_lambdaMaxOrderedPSDUpperBound #check HighDimProb.matrixQuadraticForm_nonneg_of_posSemidef +#check HighDimProb.posSemidef_of_isPSDMatrix +#check HighDimProb.matrixQuadraticForm_eq_zero_iff_mulVec_eq_zero_of_posSemidef +#check HighDimProb.matrix_mulVec_eq_zero_of_posSemidef_quadraticForm_eq_zero +#check HighDimProb.matrixQuadraticForm_eq_zero_iff_mulVec_eq_zero_of_isPSDMatrix +#check HighDimProb.matrix_mulVec_eq_zero_of_isPSDMatrix_quadraticForm_eq_zero #check HighDimProb.matrixQuadraticForm_smul_one_of_isUnitVector #check HighDimProb.rayleighUpperBound_of_spectralUpperBound #check HighDimProb.matrixQuadraticForm_le_lambdaMax_of_lambdaMax_sub_posSemidef @@ -134,6 +139,39 @@ example {n : Nat} (A : Matrix (Fin n) (Fin n) Real) 0 <= HighDimProb.matrixQuadraticForm A x := by exact HighDimProb.matrixQuadraticForm_nonneg_of_posSemidef hA x +example {n : Nat} (A : Matrix (Fin n) (Fin n) Real) + (hA : HighDimProb.IsPSDMatrix A) : + Matrix.PosSemidef A := by + exact HighDimProb.posSemidef_of_isPSDMatrix hA + +example {n : Nat} (A : Matrix (Fin n) (Fin n) Real) + (x : Fin n -> Real) (hA : A.PosSemidef) : + HighDimProb.matrixQuadraticForm A x = 0 <-> + Matrix.mulVec A x = 0 := by + exact HighDimProb.matrixQuadraticForm_eq_zero_iff_mulVec_eq_zero_of_posSemidef + hA x + +example {n : Nat} (A : Matrix (Fin n) (Fin n) Real) + (x : Fin n -> Real) (hA : A.PosSemidef) + (hx : HighDimProb.matrixQuadraticForm A x = 0) : + Matrix.mulVec A x = 0 := by + exact HighDimProb.matrix_mulVec_eq_zero_of_posSemidef_quadraticForm_eq_zero + hA hx + +example {n : Nat} (A : Matrix (Fin n) (Fin n) Real) + (x : Fin n -> Real) (hA : HighDimProb.IsPSDMatrix A) : + HighDimProb.matrixQuadraticForm A x = 0 <-> + Matrix.mulVec A x = 0 := by + exact HighDimProb.matrixQuadraticForm_eq_zero_iff_mulVec_eq_zero_of_isPSDMatrix + hA x + +example {n : Nat} (A : Matrix (Fin n) (Fin n) Real) + (x : Fin n -> Real) (hA : HighDimProb.IsPSDMatrix A) + (hx : HighDimProb.matrixQuadraticForm A x = 0) : + Matrix.mulVec A x = 0 := by + exact HighDimProb.matrix_mulVec_eq_zero_of_isPSDMatrix_quadraticForm_eq_zero + hA hx + example {n : Nat} (x : Fin n -> Real) (c : Real) (hx : HighDimProb.IsUnitVector x) : HighDimProb.matrixQuadraticForm diff --git a/HighDimProbTest/ExamplesAPI.lean b/HighDimProbTest/ExamplesAPI.lean index e16238b..beb293e 100644 --- a/HighDimProbTest/ExamplesAPI.lean +++ b/HighDimProbTest/ExamplesAPI.lean @@ -16,9 +16,39 @@ import HighDimProb.Examples.RandomMatrix.RankOnePSDUsage open HighDimProb open HighDimProb.Examples.RandomMatrix.RankOnePSDUsage +open HighDimProb.Examples.RandomMatrix.KernelNullspaceUsage variable {rankOneN : Nat} variable (rankOneV : RankOneVector rankOneN) #check (rankOneOperatorNorm_le_vectorSqNorm rankOneV : deterministicOperatorNorm (rankOneOuter rankOneV) <= vectorSqNorm rankOneV) + +variable {kernelN : Nat} +variable (kernelA : Matrix (Fin (kernelN + 1)) (Fin (kernelN + 1)) Real) +variable (kernelX : Fin (kernelN + 1) -> Real) +variable (kernelHPSD : Matrix.PosSemidef kernelA) +variable (kernelHExplicitPSD : IsPSDMatrix kernelA) + +#check matrixAction_eq_mulVec +#check invisible_of_quadraticNull_of_posSemidef +#check invisible_of_quadraticNull_of_psd +#check randomInvisible_of_quadraticNull_of_posSemidef +#check randomInvisible_of_quadraticNull_of_psd +#check psdQuadraticNullImpliesInvisible_of_core + +example : + matrixAction kernelA kernelX = Matrix.mulVec kernelA kernelX := by + exact matrixAction_eq_mulVec kernelA kernelX + +example (hNull : KernelQuadraticNullDirection kernelA kernelX) : + KernelInvisibleDirection kernelA kernelX := by + exact invisible_of_quadraticNull_of_posSemidef kernelHPSD hNull + +example (hNull : KernelQuadraticNullDirection kernelA kernelX) : + KernelInvisibleDirection kernelA kernelX := by + exact invisible_of_quadraticNull_of_psd kernelHExplicitPSD hNull + +example : + PSDQuadraticNullImpliesInvisible kernelA := by + exact psdQuadraticNullImpliesInvisible_of_core kernelA diff --git a/HighDimProbTest/RandomMatrixSpectralAPI.lean b/HighDimProbTest/RandomMatrixSpectralAPI.lean index cff1a05..9a2c07b 100644 --- a/HighDimProbTest/RandomMatrixSpectralAPI.lean +++ b/HighDimProbTest/RandomMatrixSpectralAPI.lean @@ -8,6 +8,8 @@ variable {n : Nat} variable (A : RandomMatrix Omega n n) variable (M : Matrix (Fin n) (Fin n) Real) variable (x : Fin n -> Real) +variable (hMPSD : Matrix.PosSemidef M) +variable (hMExplicitPSD : IsPSDMatrix M) variable (L : Real) variable (t : Real) variable (Z : Omega -> Real) @@ -50,6 +52,11 @@ variable (hB : forall omega, IsSelfAdjointMatrix (B omega)) #check spectralUpperBound_of_lambdaMaxPSDUpperBound #check spectralUpperBound_of_lambdaMaxOrderedPSDUpperBound #check matrixQuadraticForm_nonneg_of_posSemidef +#check posSemidef_of_isPSDMatrix +#check matrixQuadraticForm_eq_zero_iff_mulVec_eq_zero_of_posSemidef +#check matrix_mulVec_eq_zero_of_posSemidef_quadraticForm_eq_zero +#check matrixQuadraticForm_eq_zero_iff_mulVec_eq_zero_of_isPSDMatrix +#check matrix_mulVec_eq_zero_of_isPSDMatrix_quadraticForm_eq_zero #check matrixQuadraticForm_smul_one_of_isUnitVector #check rayleighUpperBound_of_spectralUpperBound #check matrixQuadraticForm_le_lambdaMax_of_lambdaMax_sub_posSemidef @@ -165,6 +172,28 @@ example (hPSD : M.PosSemidef) : 0 <= matrixQuadraticForm M x := by exact matrixQuadraticForm_nonneg_of_posSemidef hPSD x +example : + Matrix.PosSemidef M := by + exact posSemidef_of_isPSDMatrix hMExplicitPSD + +example : + matrixQuadraticForm M x = 0 <-> Matrix.mulVec M x = 0 := by + exact matrixQuadraticForm_eq_zero_iff_mulVec_eq_zero_of_posSemidef hMPSD x + +example (hx : matrixQuadraticForm M x = 0) : + Matrix.mulVec M x = 0 := by + exact matrix_mulVec_eq_zero_of_posSemidef_quadraticForm_eq_zero hMPSD hx + +example : + matrixQuadraticForm M x = 0 <-> Matrix.mulVec M x = 0 := by + exact matrixQuadraticForm_eq_zero_iff_mulVec_eq_zero_of_isPSDMatrix + hMExplicitPSD x + +example (hx : matrixQuadraticForm M x = 0) : + Matrix.mulVec M x = 0 := by + exact matrix_mulVec_eq_zero_of_isPSDMatrix_quadraticForm_eq_zero + hMExplicitPSD hx + example (hx : IsUnitVector x) : matrixQuadraticForm (t • (1 : Matrix (Fin n) (Fin n) Real)) x = t := by exact matrixQuadraticForm_smul_one_of_isUnitVector t hx diff --git a/docs/AbstractionLog.md b/docs/AbstractionLog.md index 0782596..25bcf9d 100644 --- a/docs/AbstractionLog.md +++ b/docs/AbstractionLog.md @@ -1231,7 +1231,7 @@ - Review decision: independent code review approved the change; architectural review flagged the risk that centered APIs can look analytically stronger than they are, so Lean comments and docs now state the explicit-bound-only boundary. -- Future upgrade path: next handle PSD nullspace converse as a separate concept cluster. +- Future upgrade path: next handle RM-expectation-contraction as a separate concept cluster. ## RM vector-to-rank-one matrix measurability / integrability bridge @@ -1248,6 +1248,22 @@ - Layering decision: keep the object/measurability bridge in `Basic.lean` and integrability bridges in `Expectation.lean`, where `IntegrableRandomMatrix` is defined. -- Future upgrade path: next handle PSD nullspace converse as a separate concept - cluster; expectation contraction and Matrix Bernstein tails remain out of +- Future upgrade path: next handle RM-expectation-contraction as a separate concept + cluster; Matrix Bernstein tails remain out of scope. + + +## RM PSD nullspace converse bridge + +- Concrete version chosen: wrap Mathlib's `Matrix.PosSemidef.dotProduct_mulVec_zero_iff` + in HighDimProb's explicit `matrixQuadraticForm` vocabulary, then provide the + `IsPSDMatrix` conversion through `posSemidef_of_isPSDMatrix`. +- Layering decision: keep the core deterministic bridge in `Spectral.lean` and + route the examples-local kernel/invisible-direction adapter through it, + instead of keeping a local compatibility predicate as the only API. +- Source/comment decision: theorem comments cite public PSD-square-root and + nullspace-converse references so readers can verify the mathematical fact. +- Boundary decision: this stage proves only deterministic PSD kernel facts; it + does not infer expectation contraction, covariance PSD from integrability, or + Matrix Bernstein tail statements. +- Future upgrade path: next handle RM-expectation-contraction as a separate concept cluster. diff --git a/docs/BookProgress.md b/docs/BookProgress.md index 2755d5a..5563dbc 100644 --- a/docs/BookProgress.md +++ b/docs/BookProgress.md @@ -992,8 +992,7 @@ squared-norm bounds into `BoundedOperatorNorm` and `PointwiseOperatorNormBound` for rank-one random matrices. This is not a centered summand bound, not a vector-to-matrix -measurability/integrability bridge, not a PSD nullspace converse, and not a -Matrix Bernstein tail theorem. Next safe task: RM-PSD-nullspace-converse. +measurability/integrability bridge, not a Matrix Bernstein tail theorem. Next safe task: RM-expectation-contraction. ## RM centered operator-norm prerequisite progress @@ -1014,7 +1013,7 @@ The deterministic lemma packages the matrix operator-norm triangle inequality contraction theorem and does not prove entrywise integrability or vector-to-rank-one measurability. -Next safe task: RM-PSD-nullspace-converse. +Next safe task: RM-expectation-contraction. ## RM vector-to-rank-one matrix measurability / integrability prerequisite progress @@ -1032,7 +1031,28 @@ The bridge defines the rank-one random matrix entrywise as `X_i * X_j`, proves entrywise measurability from `IsRandomVector`, and proves entrywise integrability only under explicit product-integrability assumptions or explicit coordinate `MemLp ... 2` assumptions. It does not prove integrability from -measurability alone, expectation contraction, PSD nullspace converse, or Matrix +measurability alone, expectation contraction, Matrix Bernstein tails. -Next safe task: RM-PSD-nullspace-converse. +Next safe task: RM-expectation-contraction. + + +## RM PSD nullspace converse prerequisite progress + +The PSD nullspace converse prerequisite slice is proved: + +```lean +posSemidef_of_isPSDMatrix +matrixQuadraticForm_eq_zero_iff_mulVec_eq_zero_of_posSemidef +matrix_mulVec_eq_zero_of_posSemidef_quadraticForm_eq_zero +matrixQuadraticForm_eq_zero_iff_mulVec_eq_zero_of_isPSDMatrix +matrix_mulVec_eq_zero_of_isPSDMatrix_quadraticForm_eq_zero +``` + +The core bridge wraps Mathlib's `Matrix.PosSemidef.dotProduct_mulVec_zero_iff` +into HighDimProb's explicit `matrixQuadraticForm` and `IsPSDMatrix` vocabulary. +The examples layer now derives invisible/kernel directions from PSD +quadratic-null directions through the core declarations. This is not an +expectation contraction theorem and not a Matrix Bernstein tail theorem. + +Next safe task: RM-expectation-contraction. diff --git a/docs/MatrixBernsteinProofPlan.md b/docs/MatrixBernsteinProofPlan.md index f89e218..f461899 100644 --- a/docs/MatrixBernsteinProofPlan.md +++ b/docs/MatrixBernsteinProofPlan.md @@ -41,16 +41,18 @@ Tropp/Lieb, Golden-Thompson, the Bernstein CFC primitive, the `t = 0` endpoint for the optimized wrapper, lambda-max/operator-norm Matrix Bernstein tails, or the full Matrix Bernstein tail theorem. -Next safe task: `RM-PSD-nullspace-converse`. +Next safe task: `RM-expectation-contraction`. RM prerequisite update: the centered operator-norm bridge is now proved via `deterministicOperatorNorm_sub_le_add` and the explicit-expectation-bound wrappers in `Assumptions.lean`. The vector-to-rank-one matrix bridge is also proved via `rankOneRandomMatrix`, `isRandomMatrix_rankOneRandomMatrix`, `integrableRandomMatrix_rankOneRandomMatrix_of_integrable_products`, and -`integrableRandomMatrix_rankOneRandomMatrix_of_memLp_two`. It does not prove -PSD nullspace converse, expectation contraction, or integrability from -measurability alone. +`integrableRandomMatrix_rankOneRandomMatrix_of_memLp_two`. The PSD nullspace +converse bridge is proved via `posSemidef_of_isPSDMatrix`, +`matrixQuadraticForm_eq_zero_iff_mulVec_eq_zero_of_posSemidef`, and the +one-way Mathlib-/explicit-PSD kernel wrappers. It does not prove expectation +contraction or integrability from measurability alone. ## Target Theorem diff --git a/docs/MatrixConcentrationPlan.md b/docs/MatrixConcentrationPlan.md index b359ad9..c15063f 100644 --- a/docs/MatrixConcentrationPlan.md +++ b/docs/MatrixConcentrationPlan.md @@ -22,16 +22,18 @@ compatibility APIs around the bounded-Bernstein lintegral Laplace route: `matrixBernsteinTraceMGFToLaplaceContract_statement` and `matrixBernsteinTraceMGFToLaplaceContract_under_primitives_statement`. -Next safe task: `RM-PSD-nullspace-converse`. +Next safe task: `RM-expectation-contraction`. RM prerequisite update: the centered operator-norm bridge is now proved via `deterministicOperatorNorm_sub_le_add` and the explicit-expectation-bound wrappers in `Assumptions.lean`. The vector-to-rank-one matrix bridge is also proved via `rankOneRandomMatrix`, `isRandomMatrix_rankOneRandomMatrix`, `integrableRandomMatrix_rankOneRandomMatrix_of_integrable_products`, and -`integrableRandomMatrix_rankOneRandomMatrix_of_memLp_two`. It does not prove -PSD nullspace converse, expectation contraction, or integrability from -measurability alone. +`integrableRandomMatrix_rankOneRandomMatrix_of_memLp_two`. The PSD nullspace +converse bridge is proved via `posSemidef_of_isPSDMatrix`, +`matrixQuadraticForm_eq_zero_iff_mulVec_eq_zero_of_posSemidef`, and the +one-way Mathlib-/explicit-PSD kernel wrappers. It does not prove expectation +contraction or integrability from measurability alone. Stage MC1 starts the matrix concentration branch after the scalar concentration closeout. It adds the assumption vocabulary, explicit matrix order vocabulary, diff --git a/docs/RandomMatrixAPI.md b/docs/RandomMatrixAPI.md index ec375d9..c4fded4 100644 --- a/docs/RandomMatrixAPI.md +++ b/docs/RandomMatrixAPI.md @@ -53,7 +53,13 @@ mainline. It is documentation only; theorem status is not upgraded here. `rankOneRandomMatrix`, `isRandomMatrix_rankOneRandomMatrix`, `integrableRandomMatrix_rankOneRandomMatrix_of_integrable_products`, and `integrableRandomMatrix_rankOneRandomMatrix_of_memLp_two`. -- Next safe task: `RM-PSD-nullspace-converse`. +- Proved PSD nullspace converse bridge: + `posSemidef_of_isPSDMatrix`, + `matrixQuadraticForm_eq_zero_iff_mulVec_eq_zero_of_posSemidef`, + `matrix_mulVec_eq_zero_of_posSemidef_quadraticForm_eq_zero`, + `matrixQuadraticForm_eq_zero_iff_mulVec_eq_zero_of_isPSDMatrix`, and + `matrix_mulVec_eq_zero_of_isPSDMatrix_quadraticForm_eq_zero`. +- Next safe task: `RM-expectation-contraction`. ## `HighDimProb/RandomMatrix/Basic.lean` @@ -127,6 +133,11 @@ mainline. It is documentation only; theorem status is not upgraded here. - `selfAdjointOperatorNormTailViaQuadraticFormStatement`: typed statement. - `lambdaMax_le_iff_quadraticForm_le_statement`: typed statement. - `operatorNorm_eq_max_abs_lambda_statement`: typed statement. +- `posSemidef_of_isPSDMatrix`: theorem, converts HighDimProb explicit PSD to Mathlib `Matrix.PosSemidef`. +- `matrixQuadraticForm_eq_zero_iff_mulVec_eq_zero_of_posSemidef`: theorem, PSD quadratic-form zero iff kernel membership. +- `matrix_mulVec_eq_zero_of_posSemidef_quadraticForm_eq_zero`: theorem, one-way Mathlib-PSD nullspace converse. +- `matrixQuadraticForm_eq_zero_iff_mulVec_eq_zero_of_isPSDMatrix`: theorem, explicit-PSD iff variant. +- `matrix_mulVec_eq_zero_of_isPSDMatrix_quadraticForm_eq_zero`: theorem, one-way explicit-PSD nullspace converse. ## `HighDimProb/RandomMatrix/OperatorNorm.lean` @@ -427,7 +438,7 @@ mainline. It is documentation only; theorem status is not upgraded here. ## Next Safe Task -RM-PSD-nullspace-converse: next prove or isolate the positive-semidefinite nullspace converse needed by covariance-style examples. Do not prove lambda-max/operator-norm Matrix Bernstein tails, Tropp/Lieb, Bernstein CFC, Golden-Thompson, expectation contraction, or the full Matrix Bernstein theorem in that stage. +RM-expectation-contraction: next audit whether the existing boundedness and expectation APIs can prove a narrow operator-norm expectation contraction wrapper, or record the exact missing assumptions. Do not prove lambda-max/operator-norm Matrix Bernstein tails, Tropp/Lieb, Bernstein CFC, Golden-Thompson, or the full Matrix Bernstein theorem in that stage. ## MB-S9 Matrix Bernstein Trace-MGF Under Primitives API @@ -451,4 +462,4 @@ RM-PSD-nullspace-converse: next prove or isolate the positive-semidefinite nulls proved in `ConcentrationStatements.lean`, with exponential-add RHS. - The theta-optimized scalar-RHS quadratic-form wrapper under primitives is now proved in `ConcentrationStatements.lean`, with Bernstein denominator RHS. -- Next safe task: RM-PSD-nullspace-converse. +- Next safe task: RM-expectation-contraction. diff --git a/docs/Status.md b/docs/Status.md index 3a4868f..3032e89 100644 --- a/docs/Status.md +++ b/docs/Status.md @@ -14,7 +14,7 @@ integrability bridges for covariance-style examples. The latest proved public theorem is: -- `integrableRandomMatrix_rankOneRandomMatrix_of_memLp_two` +- `matrix_mulVec_eq_zero_of_isPSDMatrix_quadraticForm_eq_zero` Supporting proved API also includes `rankOneRandomMatrix`, `isRandomMatrix_rankOneRandomMatrix`, @@ -27,18 +27,21 @@ rank-one operator-norm bridge `rankOneOperatorNorm_le_vectorSqNorm`, `PointwiseOperatorNormBound_rankOne_of_sqNorm_bound`. The new vector-to-matrix bridge proves entrywise measurability from `IsRandomVector`; entrywise integrability is proved only from explicit product-integrability assumptions or -explicit coordinate `MemLp ... 2` assumptions. It does not prove integrability -from measurability alone, expectation contraction, the PSD nullspace converse, -lambda-max/operator-norm Matrix Bernstein tails, Tropp/Lieb, the Bernstein CFC -primitive, Golden-Thompson, the `t = 0` endpoint for the optimized wrapper, or -the final full Matrix Bernstein tail theorem. +explicit coordinate `MemLp ... 2` assumptions. The new PSD nullspace bridge +exposes `posSemidef_of_isPSDMatrix`, +`matrixQuadraticForm_eq_zero_iff_mulVec_eq_zero_of_posSemidef`, and the +one-way Mathlib-/explicit-PSD kernel wrappers. It does not prove integrability +from measurability alone, expectation contraction, lambda-max/operator-norm +Matrix Bernstein tails, Tropp/Lieb, the Bernstein CFC primitive, +Golden-Thompson, the `t = 0` endpoint for the optimized wrapper, or the final +full Matrix Bernstein tail theorem. The previous optimized quadratic-form theorem remains `matrixBernsteinQuadraticFormUpperTailOptimizedScalarRHSWithBernsteinCoeff_under_primitives` under explicit primitive assumptions. ## Next Safe Task -- `RM-PSD-nullspace-converse` +- `RM-expectation-contraction` ## Public Milestone Summary @@ -1793,7 +1796,6 @@ theorems. Theorem statements blocked by missing infrastructure are tracked in docs/TheoremAtlas.md. -## Next safe task Stage MB-S9-trace-mgf-to-laplace-tail-contract-v2 - re-audit how the proved bounded trace-MGF theorem under explicit primitives and the proved @@ -1933,8 +1935,21 @@ matching lintegral semantic trace-MGF bound under random self-adjointness and trace-exp integrability. It does not prove event reduction, dimension/norm reduction, theta optimization, Tropp/Lieb, the Bernstein CFC primitive, Golden-Thompson, or the Matrix Bernstein tail theorem. Next safe task: -MB-S9-trace-mgf-to-laplace-tail-contract-v2. +RM-expectation-contraction. + + +Stage RM-PSD-nullspace-converse has no build blocker. The Spectral layer now +exposes `posSemidef_of_isPSDMatrix`, +`matrixQuadraticForm_eq_zero_iff_mulVec_eq_zero_of_posSemidef`, +`matrix_mulVec_eq_zero_of_posSemidef_quadraticForm_eq_zero`, +`matrixQuadraticForm_eq_zero_iff_mulVec_eq_zero_of_isPSDMatrix`, and +`matrix_mulVec_eq_zero_of_isPSDMatrix_quadraticForm_eq_zero`. The examples +layer now routes quadratic-null PSD directions to invisible/kernel directions +through the core bridge. This stage does not prove expectation contraction, +lambda-max/operator-norm Matrix Bernstein tails, Tropp/Lieb, Bernstein CFC, +Golden-Thompson, or the full Matrix Bernstein theorem. Next safe task: +RM-expectation-contraction. ## Next safe task -- `RM-PSD-nullspace-converse` +- `RM-expectation-contraction` diff --git a/docs/TODO.md b/docs/TODO.md index d7aa74c..f5c3ed3 100644 --- a/docs/TODO.md +++ b/docs/TODO.md @@ -25,14 +25,20 @@ added `rankOneRandomMatrix`, `isRandomMatrix_rankOneRandomMatrix`, `integrableRandomMatrix_rankOneRandomMatrix_of_integrable_products`, and `integrableRandomMatrix_rankOneRandomMatrix_of_memLp_two`. +- Done: PSD nullspace converse prerequisite slice added + `posSemidef_of_isPSDMatrix`, + `matrixQuadraticForm_eq_zero_iff_mulVec_eq_zero_of_posSemidef`, + `matrix_mulVec_eq_zero_of_posSemidef_quadraticForm_eq_zero`, + `matrixQuadraticForm_eq_zero_iff_mulVec_eq_zero_of_isPSDMatrix`, and + `matrix_mulVec_eq_zero_of_isPSDMatrix_quadraticForm_eq_zero`. - The optimized theorem remains one-sided, quadratic-form, and under explicit `troppMasterTraceMGFFiniteFamily_statement` plus pointwise `bernsteinMatrixExp_le_quadratic_statement` assumptions. -- Not proved: PSD nullspace converse, lambda-max/operator-norm +- Not proved: expectation contraction, lambda-max/operator-norm tail bridge, optimized `t = 0` endpoint, functional-calculus proof / Bernstein CFC primitive, full CFC-free single-summand MGF theorem, Lieb concavity, Golden-Thompson, and the full Matrix Bernstein tail theorem. -- Next: RM-PSD-nullspace-converse. +- Next: RM-expectation-contraction. ## Stage M3 Scalar Closeout TODO Audit The forward scalar subGaussian proof spine is closed as an experimental @@ -207,8 +213,8 @@ Stage H0 Rademacher/Hoeffding branch update: | Concrete trace-exp dominance assembly | Use the `lambdaMaxOrdered` spectral and trace-exp providers to prove `TraceExpDominatesQuadraticFormUpperTail` for random self-adjoint matrices. | `lambdaMaxOrdered_rayleighUpperBound`, `lambdaMaxOrdered_traceExpDominatesUpperBound`, `traceExpDominatesQuadraticFormUpperTail_of_rayleighUpperBound_of_traceExpDominatesUpperBound`, `RandomSelfAdjointMatrix` | done | Implemented in MB-S7C-assemble-dominance as `traceExpDominatesQuadraticFormUpperTail_of_randomSelfAdjoint`. This did not prove full matrix Laplace, trace-mgf, Golden-Thompson, Lieb, or Matrix Bernstein. | | Conditional matrix Laplace assembly | Use concrete random self-adjoint dominance with the existing conditional Laplace wrappers to prove the matrix Laplace upper-tail theorem. | `traceExpDominatesQuadraticFormUpperTail_of_randomSelfAdjoint`, `matrixLaplaceTransformLIntegral_of_traceExpDominatesQuadraticFormUpperTail`, explicit measurability/integrability hypotheses | done | Implemented in MB-S8-laplace-assembly as `matrixLaplaceTransformLIntegralDiv_of_randomSelfAdjoint` and `matrixLaplaceTransformLIntegral_of_randomSelfAdjoint`. This did not prove the real RHS bridge, trace-mgf, Golden-Thompson, Lieb, or Matrix Bernstein. | | Matrix Laplace real RHS bridge | Connect the lintegral matrix Laplace theorem to the existing real trace-exp moment/RHS vocabulary. | `matrixLaplaceTransformLIntegral_of_randomSelfAdjoint`, `traceExpMomentLIntegral_eq_ofReal_traceExpMoment`, explicit integrability and nonnegativity hypotheses | hard | Future task after the current trace-mgf provider contract decision; do not prove trace-mgf, Golden-Thompson, Lieb, or Matrix Bernstein in that bridge stage. | -| Matrix trace-mgf foundation/provider contract | Audit the route for proving the semantic bounded Matrix Bernstein trace-mgf target. | `TraceMGFBound`, `TraceMGFBernsteinVarianceProxyBound`, `matrixBernsteinTraceMGFWithBernsteinCoeff_statement`, matrix-valued independence, variance proxy, Golden-Thompson/Lieb or equivalent matrix-mgf machinery | hard | MB-S9-foundation added only semantic predicates and typed targets; MB-S9 follow-up stages isolated and resolved expectation, MatrixLE algebra, coefficient, lower-bound, provider-under-CFC, and RHS-normalization blockers while leaving Tropp/Lieb and Bernstein CFC primitives typed only. `matrixBernsteinTraceMGF_statement` remains a `theta ^ 2 / 2` compatibility target, not the bounded Bernstein denominator target. Current next safe task: RM-PSD-nullspace-converse. | -| Matrix exponential lower bound for Bernstein coefficient | Audit/prove the deterministic bridge `MatrixLE (1 + c smul V) (matrixExp (c smul V))` after `bernsteinCoefficient_nonneg`. | `bernsteinCoefficient_nonneg`, `MatrixLE`, `matrixExp`, PSD/self-adjoint variance proxy hypotheses, CFC or spectral exponential lower APIs | done | MB-S9-exp-lower-bound-proof implements this deterministic lower-bound family as `matrixLE_one_add_self_le_matrixExp_of_selfAdjoint` and `matrixLE_one_add_smul_le_matrixExp_smul_of_selfAdjoint`. MB-S9-single-summand-provider-under-cfc then uses it in `singleSummandMatrixMGFVarianceProxy_of_bernsteinMatrixExp_le_quadratic`. MB-S9-rhs-normalization-proof names the denominator coefficient as `bernsteinMGFCoeff` and adds bounded trace-mgf targets. The Bernstein CFC proof, trace-mgf provider, Golden-Thompson, Lieb, and Matrix Bernstein remain unproved. Next safe task: RM-PSD-nullspace-converse. | +| Matrix trace-mgf foundation/provider contract | Audit the route for proving the semantic bounded Matrix Bernstein trace-mgf target. | `TraceMGFBound`, `TraceMGFBernsteinVarianceProxyBound`, `matrixBernsteinTraceMGFWithBernsteinCoeff_statement`, matrix-valued independence, variance proxy, Golden-Thompson/Lieb or equivalent matrix-mgf machinery | hard | MB-S9-foundation added only semantic predicates and typed targets; MB-S9 follow-up stages isolated and resolved expectation, MatrixLE algebra, coefficient, lower-bound, provider-under-CFC, and RHS-normalization blockers while leaving Tropp/Lieb and Bernstein CFC primitives typed only. `matrixBernsteinTraceMGF_statement` remains a `theta ^ 2 / 2` compatibility target, not the bounded Bernstein denominator target. Current next safe task: RM-expectation-contraction. | +| Matrix exponential lower bound for Bernstein coefficient | Audit/prove the deterministic bridge `MatrixLE (1 + c smul V) (matrixExp (c smul V))` after `bernsteinCoefficient_nonneg`. | `bernsteinCoefficient_nonneg`, `MatrixLE`, `matrixExp`, PSD/self-adjoint variance proxy hypotheses, CFC or spectral exponential lower APIs | done | MB-S9-exp-lower-bound-proof implements this deterministic lower-bound family as `matrixLE_one_add_self_le_matrixExp_of_selfAdjoint` and `matrixLE_one_add_smul_le_matrixExp_smul_of_selfAdjoint`. MB-S9-single-summand-provider-under-cfc then uses it in `singleSummandMatrixMGFVarianceProxy_of_bernsteinMatrixExp_le_quadratic`. MB-S9-rhs-normalization-proof names the denominator coefficient as `bernsteinMGFCoeff` and adds bounded trace-mgf targets. The Bernstein CFC proof, trace-mgf provider, Golden-Thompson, Lieb, and Matrix Bernstein remain unproved. Next safe task: RM-expectation-contraction. | ## MB-S9 Tropp Shape Refactor Follow-Up The trace-exp layer now exposes `troppMasterTraceMGFFiniteFamily_statement`, @@ -223,7 +229,7 @@ safe task: MB-S9-trace-mgf-to-laplace-tail-contract. - Still unproved: the finite-family Tropp/Lieb primitive itself. - Still unproved: the Bernstein CFC primitive. - Still unproved: Lieb, Golden-Thompson, and the Matrix Bernstein tail theorem. -- Next safe task: RM-PSD-nullspace-converse. +- Next safe task: RM-expectation-contraction. ## MB-S9 Matrix Bernstein Trace-MGF Under Primitives Follow-Up @@ -232,4 +238,4 @@ safe task: MB-S9-trace-mgf-to-laplace-tail-contract. and pointwise `bernsteinMatrixExp_le_quadratic_statement`. - Still unproved: finite-family Tropp/Lieb primitive, Bernstein CFC primitive, Lieb, Golden-Thompson, and Matrix Bernstein tail theorem. -- Next safe task: RM-PSD-nullspace-converse. +- Next safe task: RM-expectation-contraction. diff --git a/docs/TermMap.md b/docs/TermMap.md index 6f4c1b4..0d7963a 100644 --- a/docs/TermMap.md +++ b/docs/TermMap.md @@ -131,10 +131,11 @@ Note: some declarations exist as scaffolds, but the corresponding concept is not | Squared operator-norm bound predicate | Matrix concentration prerequisites | Pointwise squared matrix-vector bound over all explicit unit vectors. | `IsUnitVector`, `matVecSqNorm`, `Matrix.Norms.L2Operator` | `OperatorNormBoundSq`, `RandomOperatorNormBoundSq`, `matVecSqNorm_le_of_operatorNormBoundSq`, `operatorNorm_le_of_operatorNormBoundSq`, `operatorNormBoundSq_of_operatorNorm_le` | `HighDimProb/RandomMatrix/OperatorNorm.lean` | implemented/proven experimental API | The explicit predicate is retained for theorem statements and is now bridged in both directions with `deterministicOperatorNorm` under the visible nonnegative-scale hypotheses. | | Exact operator-norm bridge targets | Matrix concentration prerequisites | Typed targets and proved bridges connecting explicit squared unit-vector bounds to Mathlib's scoped L2 matrix norm and measurability. | `Matrix.Norms.L2Operator`, product measurable spaces, `measurable_norm` | `operatorNorm_le_of_operatorNormBoundSqStatement`, `operatorNormBoundSq_of_operatorNorm_leStatement`, `operatorNormMeasurabilityStatement`, `operatorNorm_le_of_operatorNormBoundSq`, `operatorNormBoundSq_of_operatorNorm_le`, `instOpensMeasurableSpaceMatrixL2Operator`, `isRealRandomVariable_operatorNorm` | `HighDimProb/RandomMatrix/OperatorNorm.lean` | proven bridge plus typed-prop compatibility targets | Stage MC2-fix proves the exact comparison directions and operator-norm measurability; the statement-only targets remain as API signposts. | | Rank-one operator-norm bound | Rank-one covariance and matrix-concentration prerequisites | The self-outer product `v vᵀ` has induced L2 operator norm bounded by `||v||₂²`. | `Matrix.Norms.L2Operator`, `ContinuousLinearMap.opNorm_le_bound`, Cauchy-Schwarz | `rankOneOperatorNorm_le_vectorSqNorm` | `HighDimProb/RandomMatrix/OperatorNorm.lean` | proven experimental API | The proof uses the existing `deterministicOperatorNorm` convention and does not introduce new rank-one vocabulary. | -| Rank-one pointwise operator-norm bound | Matrix Bernstein boundedness prerequisites | A pointwise squared-vector-norm bound implies a pointwise operator-norm bound for `omega |-> X omega X omegaᵀ` and indexed families. | `operatorNorm`, `vectorSqNorm`, `PointwiseOperatorNormBound` | `BoundedOperatorNorm_rankOne_of_sqNorm_bound`, `PointwiseOperatorNormBound_rankOne_of_sqNorm_bound` | `HighDimProb/RandomMatrix/Assumptions.lean` | proven experimental API | This is a boundedness bridge only; centered expectation bounds, measurability/integrability bridges, and PSD nullspace converse remain separate tasks. | +| Rank-one pointwise operator-norm bound | Matrix Bernstein boundedness prerequisites | A pointwise squared-vector-norm bound implies a pointwise operator-norm bound for `omega |-> X omega X omegaᵀ` and indexed families. | `operatorNorm`, `vectorSqNorm`, `PointwiseOperatorNormBound` | `BoundedOperatorNorm_rankOne_of_sqNorm_bound`, `PointwiseOperatorNormBound_rankOne_of_sqNorm_bound` | `HighDimProb/RandomMatrix/Assumptions.lean` | proven experimental API | This is a boundedness bridge only; centered expectation bounds, measurability/integrability bridges, and PSD nullspace converse are handled as separate tasks. | | Centered operator-norm bound | Matrix Bernstein boundedness prerequisites | Centering satisfies `||X(ω) - E X||op <= ||X(ω)||op + ||E X||op`; a pointwise bound plus explicit expectation bound yields a bound on `centeredRandomMatrix`. | `norm_sub_le`, `matrixExpect`, `centeredRandomMatrix`, `PointwiseOperatorNormBound` | `deterministicOperatorNorm_sub_le_add`, `BoundedOperatorNorm_centered_of_bound_expect_bound`, `PointwiseOperatorNormBound_centered_of_bound_expect_bound`, `PointwiseOperatorNormBound_centered_of_bound_expect_bound_same` | `HighDimProb/RandomMatrix/OperatorNorm.lean`, `HighDimProb/RandomMatrix/Assumptions.lean` | proven experimental API | Algebraic explicit-bound wrapper only; it does not prove entrywise integrability, vector-to-rank-one measurability, or expectation operator-norm contraction. | +| PSD nullspace converse | Matrix Bernstein covariance-style prerequisites | For a real PSD matrix, a zero quadratic form `xᵀ A x = 0` is equivalent to `A x = 0`; HighDimProb exposes both Mathlib `Matrix.PosSemidef` and explicit `IsPSDMatrix` variants. | `Matrix.PosSemidef.dotProduct_mulVec_zero_iff`, `matrixQuadraticForm`, `Matrix.mulVec`, `IsPSDMatrix` | `posSemidef_of_isPSDMatrix`, `matrixQuadraticForm_eq_zero_iff_mulVec_eq_zero_of_posSemidef`, `matrix_mulVec_eq_zero_of_posSemidef_quadraticForm_eq_zero`, `matrixQuadraticForm_eq_zero_iff_mulVec_eq_zero_of_isPSDMatrix`, `matrix_mulVec_eq_zero_of_isPSDMatrix_quadraticForm_eq_zero` | `HighDimProb/RandomMatrix/Spectral.lean`, `HighDimProb/Examples/RandomMatrix/KernelNullspaceUsage.lean` | proven experimental API | This is a deterministic PSD kernel bridge only; it does not prove expectation contraction or Matrix Bernstein tails. | | Matrix symmetry/self-adjointness | Matrix Bernstein prerequisites | Pointwise real symmetric/self-adjoint matrix predicates and random-matrix wrappers. | `Matrix.IsSymm`, `Matrix.IsHermitian` | `IsSymmetricMatrix`, `IsSelfAdjointMatrix`, `RandomSymmetricMatrix`, `RandomSelfAdjointMatrix` | `HighDimProb/RandomMatrix/SelfAdjoint.lean` | implemented experimental API | Stage MC1 keeps the vocabulary explicit and does not prove spectral theorems. | -| Vector-to-rank-one matrix measurability / integrability | Matrix Bernstein covariance-style prerequisites | A random vector `X` defines the rank-one random matrix with entries `X_i X_j`; entrywise measurability follows from coordinate measurability, while entrywise integrability requires explicit product or square-moment assumptions. | `Measurable.mul`, `MemLp.integrable_mul`, `IsRandomVector`, `IntegrableRandomMatrix` | `rankOneRandomMatrix`, `isRandomMatrix_rankOneRandomMatrix`, `integrableRandomMatrix_rankOneRandomMatrix_of_integrable_products`, `integrableRandomMatrix_rankOneRandomMatrix_of_memLp_two` | `HighDimProb/RandomMatrix/Basic.lean`, `HighDimProb/RandomMatrix/Expectation.lean` | proven experimental API | This bridge deliberately separates measurability from integrability and does not prove PSD nullspace converse or expectation contraction. | +| Vector-to-rank-one matrix measurability / integrability | Matrix Bernstein covariance-style prerequisites | A random vector `X` defines the rank-one random matrix with entries `X_i X_j`; entrywise measurability follows from coordinate measurability, while entrywise integrability requires explicit product or square-moment assumptions. | `Measurable.mul`, `MemLp.integrable_mul`, `IsRandomVector`, `IntegrableRandomMatrix` | `rankOneRandomMatrix`, `isRandomMatrix_rankOneRandomMatrix`, `integrableRandomMatrix_rankOneRandomMatrix_of_integrable_products`, `integrableRandomMatrix_rankOneRandomMatrix_of_memLp_two` | `HighDimProb/RandomMatrix/Basic.lean`, `HighDimProb/RandomMatrix/Expectation.lean` | proven experimental API | This bridge deliberately separates measurability from integrability and does not prove expectation contraction. | | PSD and Loewner-style order | Matrix Bernstein and covariance prerequisites | PSD means symmetric plus nonnegative quadratic forms; `MatrixLE A B` means `B - A` is PSD. | finite sums, explicit quadratic forms | `matrixQuadraticForm`, `IsPSDMatrix`, `RandomPSDMatrix`, `MatrixLE`, `quadraticForm_le_of_matrixLE` | `HighDimProb/RandomMatrix/MatrixOrder.lean` | implemented/proven experimental API | No global matrix order instance is installed. Stage MC2 proves the quadratic-form monotonicity bridge for the explicit Loewner-style order. | | MatrixLE / PSD algebra | Matrix Bernstein single-summand MGF route | Small algebra for explicit PSD and Loewner-style order: addition, nonnegative scalar multiplication, reflexivity, equality, transitivity, and add/smul monotonicity. | explicit quadratic forms, matrix add/sub/smul | `matrixQuadraticForm_add`, `matrixQuadraticForm_smul`, `isPSDMatrix_zero`, `isPSDMatrix_add`, `isPSDMatrix_smul_of_nonneg`, `matrixLE_refl`, `matrixLE_of_eq`, `matrixLE_trans`, `matrixLE_add`, `matrixLE_add_left`, `matrixLE_add_right`, `matrixLE_smul_of_nonneg` | `HighDimProb/RandomMatrix/MatrixOrder.lean` | proven experimental API | MB-S9-matrixle-algebra-proof closes the MatrixLE algebra/RHS-normalization blocker; the Bernstein CFC proof, single-summand MGF provider, trace-mgf provider, and Matrix Bernstein remain unproved. | | Matrix expectation and centering | Matrix concentration prerequisites | Entrywise expectation, entrywise integrability, and entrywise centering for random matrices. | `expect`, `matrixEntry`, `IntegrableRealRandomVariable` | `matrixExpect`, `IntegrableRandomMatrix`, `centeredRandomMatrix` | `HighDimProb/RandomMatrix/Expectation.lean` | implemented experimental API | This avoids committing to Bochner expectation before theorem proofs require it. | diff --git a/docs/TheoremAtlas.md b/docs/TheoremAtlas.md index 6027d60..a5a5744 100644 --- a/docs/TheoremAtlas.md +++ b/docs/TheoremAtlas.md @@ -30,7 +30,7 @@ statement APIs connecting bounded Bernstein lintegral trace-MGF bounds to the existing Laplace/tail layer without claiming the missing real-to-lintegral, Tropp/Lieb, CFC, or Matrix Bernstein proofs. -Next safe task: `RM-PSD-nullspace-converse`. +Next safe task: `RM-expectation-contraction`. ## Milestone 3 scalar implication closeout This audit separates proved theorem families from typed statements and blocked @@ -1247,7 +1247,7 @@ future directions. `HighDimProbTest/RandomMatrixLaplaceAPI.lean`, and `HighDimProbTest/RandomMatrixConcentrationAPI.lean`. - Priority: Stage MB-S2 through MB-S9-foundation complete; next task is - RM-PSD-nullspace-converse. + RM-expectation-contraction. ## Trace-Exponential Positivity Bridge (MB-S3/MB-S4) @@ -1645,7 +1645,7 @@ future directions. `HighDimProbJudge/RandomMatrix/VarianceProxyUse.lean`, `HighDimProbJudge/RandomMatrix/MatrixBernsteinUse.lean`, and `HighDimProbJudge/RandomMatrix/StatementUse.lean`. -- Priority: next safe task is RM-PSD-nullspace-converse. +- Priority: next safe task is RM-expectation-contraction. ## PSD of Matrix Square / Second Moment / Variance Proxy (MB-S1) @@ -1821,7 +1821,7 @@ future directions. - Target module: `HighDimProb/RandomMatrix/TraceExp.lean` - Test module: `HighDimProbTest/RandomMatrixTraceExpAPI.lean` - Judge module: `HighDimProbJudge/RandomMatrix/TraceExpUse.lean` -- Priority: next safe task is RM-PSD-nullspace-converse. +- Priority: next safe task is RM-expectation-contraction. ## Matrix Exponential Lower Bound (MB-S9-exp-lower-bound-proof) @@ -1948,7 +1948,7 @@ future directions. - Blocker: the finite-family Tropp primitive itself remains typed only; the Bernstein CFC primitive remains typed only; Lieb, Golden-Thompson, and the Matrix Bernstein tail theorem remain unproved. -- Priority: next safe task is RM-PSD-nullspace-converse. +- Priority: next safe task is RM-expectation-contraction. @@ -1966,7 +1966,7 @@ future directions. - Blocker: the result is still one-sided and quadratic-form under explicit Tropp/Lieb and Bernstein CFC primitives; lambda-max/operator-norm tail bridges and the full Matrix Bernstein theorem remain unproved. -- Priority: next safe task is RM-PSD-nullspace-converse. +- Priority: next safe task is RM-expectation-contraction. ## Matrix Bernstein Trace-MGF to Laplace/Tail Contract (MB-S9) @@ -1986,7 +1986,7 @@ future directions. - Blocker: prove or sharpen the real trace-MGF to lintegral bridge; keep the event-subset, Tropp/Lieb, Bernstein CFC, Golden-Thompson, and Matrix Bernstein tail theorem gaps explicit. -- Priority: next safe task is RM-PSD-nullspace-converse. +- Priority: next safe task is RM-expectation-contraction. ## RM Centered Operator-Norm Bound @@ -2002,8 +2002,8 @@ future directions. - Status: proven, API-tested, and judge-tested. - Blocker: this is only an algebraic explicit-bound wrapper. It does not prove vector-to-rank-one matrix measurability/integrability, expectation - contraction, PSD nullspace converse, or Matrix Bernstein tails. -- Priority: next safe task is RM-PSD-nullspace-converse. + contraction, Matrix Bernstein tails. +- Priority: next safe task is RM-expectation-contraction. ## RM Vector-to-Rank-One Matrix Measurability / Integrability @@ -2018,5 +2018,24 @@ future directions. `integrableRandomMatrix_rankOneRandomMatrix_of_memLp_two`. - Status: proven, API-tested, and judge-tested. - Blocker: this does not prove integrability from measurability alone, - expectation contraction, PSD nullspace converse, or Matrix Bernstein tails. -- Priority: next safe task is RM-PSD-nullspace-converse. + expectation contraction, Matrix Bernstein tails. +- Priority: next safe task is RM-expectation-contraction. + + +## RM PSD Nullspace Converse + +- Informal statement: for a real positive semidefinite matrix `A`, the zero + quadratic-form condition `xᵀ A x = 0` is equivalent to the kernel condition + `A x = 0`; HighDimProb exposes this in both Mathlib `Matrix.PosSemidef` and + explicit `IsPSDMatrix` vocabulary. +- Target Lean declarations: + `posSemidef_of_isPSDMatrix`, + `matrixQuadraticForm_eq_zero_iff_mulVec_eq_zero_of_posSemidef`, + `matrix_mulVec_eq_zero_of_posSemidef_quadraticForm_eq_zero`, + `matrixQuadraticForm_eq_zero_iff_mulVec_eq_zero_of_isPSDMatrix`, and + `matrix_mulVec_eq_zero_of_isPSDMatrix_quadraticForm_eq_zero`. +- Status: proven, API-tested, and judge-tested. +- Blocker: this is only a deterministic PSD kernel bridge. It does not prove + expectation contraction, covariance expectation identities, or Matrix + Bernstein tails. +- Priority: next safe task is RM-expectation-contraction. From 70bc7516270995a73016a94406cc3b5d29f04cf1 Mon Sep 17 00:00:00 2001 From: dududuguo Date: Sat, 13 Jun 2026 23:12:00 +1000 Subject: [PATCH 2/2] Use named rank-one matrix APIs --- HighDimProb/RandomMatrix/Assumptions.lean | 24 +++++++++---------- HighDimProb/RandomMatrix/Basic.lean | 20 +++++++++++++++- HighDimProb/RandomMatrix/OperatorNorm.lean | 6 ++--- .../RandomMatrix/OperatorNormUse.lean | 11 ++++----- HighDimProbTest/ExamplesAPI.lean | 2 +- .../RandomMatrixAssumptionsAPI.lean | 9 ++++--- HighDimProbTest/RandomMatrixBasicAPI.lean | 6 +++++ .../RandomMatrixOperatorNormAPI.lean | 9 +++---- docs/AbstractionLog.md | 10 ++++---- docs/BookProgress.md | 4 ++-- docs/RandomMatrixAPI.md | 14 ++++++----- docs/Status.md | 4 ++-- docs/TODO.md | 4 ++-- docs/TermMap.md | 4 ++-- 14 files changed, 75 insertions(+), 52 deletions(-) diff --git a/HighDimProb/RandomMatrix/Assumptions.lean b/HighDimProb/RandomMatrix/Assumptions.lean index 3a4298c..31eab6e 100644 --- a/HighDimProb/RandomMatrix/Assumptions.lean +++ b/HighDimProb/RandomMatrix/Assumptions.lean @@ -94,19 +94,18 @@ def BoundedOperatorNorm {Omega : Type*} [MeasurableSpace Omega] {m n : Nat} /-- A pointwise squared-vector-norm bound gives an operator-norm bound for the -rank-one random matrix `omega |-> X(omega) X(omega)^T`. +named rank-one random matrix `rankOneRandomMatrix X`. Formula reference: the deterministic ingredient is `||v v^T||op <= ||v||_2^2` for a rank-one outer product; see https://en.wikipedia.org/wiki/Outer_product and https://en.wikipedia.org/wiki/Operator_norm -/ -theorem BoundedOperatorNorm_rankOne_of_sqNorm_bound {Omega : Type*} +theorem BoundedOperatorNorm_rankOneRandomMatrix_of_sqNorm_bound {Omega : Type*} [MeasurableSpace Omega] {n : Nat} - (X : Omega -> Fin n -> Real) (R : Real) - (_hR : 0 <= R) + (X : RandomVector Omega n) (R : Real) (hX : forall omega, vectorSqNorm (X omega) <= R) : - BoundedOperatorNorm (fun omega i j => X omega i * X omega j) R := by + BoundedOperatorNorm (rankOneRandomMatrix X) R := by intro omega exact (rankOneOperatorNorm_le_vectorSqNorm (X omega)).trans (hX omega) @@ -152,23 +151,22 @@ def PointwiseOperatorNormBound {Omega : Type*} [MeasurableSpace Omega] forall i, BoundedOperatorNorm (A i) R /-- -Family version of the rank-one operator-norm bridge: if every vector sample has -`vectorSqNorm <= R`, then the associated rank-one matrix family is pointwise -operator-norm bounded by `R`. +Family version of the named rank-one operator-norm bridge: if every vector +sample has `vectorSqNorm <= R`, then the associated rank-one matrix family is +pointwise operator-norm bounded by `R`. Formula reference: this packages the outer-product bound `||v v^T||op <= ||v||_2^2`; see https://en.wikipedia.org/wiki/Outer_product and https://en.wikipedia.org/wiki/Operator_norm -/ -theorem PointwiseOperatorNormBound_rankOne_of_sqNorm_bound {Omega : Type*} +theorem PointwiseOperatorNormBound_rankOneRandomMatrix_of_sqNorm_bound {Omega : Type*} [MeasurableSpace Omega] {I : Type*} {n : Nat} - (X : I -> Omega -> Fin n -> Real) (R : Real) - (hR : 0 <= R) + (X : I -> RandomVector Omega n) (R : Real) (hX : forall i omega, vectorSqNorm (X i omega) <= R) : - PointwiseOperatorNormBound (fun i omega a b => X i omega a * X i omega b) R := by + PointwiseOperatorNormBound (fun i => rankOneRandomMatrix (X i)) R := by intro i - exact BoundedOperatorNorm_rankOne_of_sqNorm_bound (X i) R hR (hX i) + exact BoundedOperatorNorm_rankOneRandomMatrix_of_sqNorm_bound (X i) R (hX i) /-- Family version of the centered operator-norm bridge under an explicit bound on diff --git a/HighDimProb/RandomMatrix/Basic.lean b/HighDimProb/RandomMatrix/Basic.lean index 4cabeb1..98061ef 100644 --- a/HighDimProb/RandomMatrix/Basic.lean +++ b/HighDimProb/RandomMatrix/Basic.lean @@ -64,6 +64,24 @@ theorem matrixEntry_apply {Omega : Type*} [MeasurableSpace Omega] {m n : Nat} matrixEntry A i j omega = A omega i j := rfl +/-- +Deterministic rank-one self outer-product matrix associated to a vector. + +Formula reference: the outer product has entries `x_i * x_j`; see +https://en.wikipedia.org/wiki/Outer_product . +-/ +def rankOneMatrix {n : Nat} (x : Fin n -> Real) : Matrix (Fin n) (Fin n) Real := + fun i j => x i * x j + +/-- +Formula reference: this unfolds the rank-one outer-product entry `x_i * x_j`; +see https://en.wikipedia.org/wiki/Outer_product . +-/ +@[simp] +theorem rankOneMatrix_apply {n : Nat} (x : Fin n -> Real) (i j : Fin n) : + rankOneMatrix x i j = x i * x j := + rfl + /-- Rank-one self outer-product random matrix associated to a random vector. @@ -75,7 +93,7 @@ https://en.wikipedia.org/wiki/Random_vector . -/ def rankOneRandomMatrix {Omega : Type*} [MeasurableSpace Omega] {n : Nat} (X : RandomVector Omega n) : RandomMatrix Omega n n := - fun omega i j => X omega i * X omega j + fun omega => rankOneMatrix (X omega) /-- Formula reference: this unfolds the rank-one outer-product entry diff --git a/HighDimProb/RandomMatrix/OperatorNorm.lean b/HighDimProb/RandomMatrix/OperatorNorm.lean index 4f70edc..22eb5a9 100644 --- a/HighDimProb/RandomMatrix/OperatorNorm.lean +++ b/HighDimProb/RandomMatrix/OperatorNorm.lean @@ -109,18 +109,18 @@ https://en.wikipedia.org/wiki/Operator_norm -/ theorem rankOneOperatorNorm_le_vectorSqNorm {n : Nat} (v : Fin n -> Real) : - deterministicOperatorNorm (fun i j : Fin n => v i * v j) <= vectorSqNorm v := by + deterministicOperatorNorm (rankOneMatrix v) <= vectorSqNorm v := by rw [deterministicOperatorNorm, Matrix.l2_opNorm_def] refine ContinuousLinearMap.opNorm_le_bound _ (vectorSqNorm_nonneg v) ?_ intro y have happly : (((Matrix.toEuclideanLin (𝕜 := Real) (m := Fin n) (n := Fin n)).trans LinearMap.toContinuousLinearMap) - (fun i j : Fin n => v i * v j) y) = + (rankOneMatrix v) y) = (inner Real (WithLp.toLp 2 v : EuclideanSpace Real (Fin n)) y) • (WithLp.toLp 2 v : EuclideanSpace Real (Fin n)) := by ext i - simp [Matrix.toLpLin_apply, Matrix.mulVec, dotProduct, inner] + simp [rankOneMatrix, Matrix.toLpLin_apply, Matrix.mulVec, dotProduct, inner] rw [Finset.sum_mul] apply Finset.sum_congr rfl intro j _ diff --git a/HighDimProbJudge/RandomMatrix/OperatorNormUse.lean b/HighDimProbJudge/RandomMatrix/OperatorNormUse.lean index 1dbb5a9..50ec4fa 100644 --- a/HighDimProbJudge/RandomMatrix/OperatorNormUse.lean +++ b/HighDimProbJudge/RandomMatrix/OperatorNormUse.lean @@ -3,8 +3,8 @@ import HighDimProb.RandomMatrix #check HighDimProb.isRealRandomVariable_operatorNorm #check HighDimProb.deterministicOperatorNorm_sub_le_add #check HighDimProb.rankOneOperatorNorm_le_vectorSqNorm -#check HighDimProb.BoundedOperatorNorm_rankOne_of_sqNorm_bound -#check HighDimProb.PointwiseOperatorNormBound_rankOne_of_sqNorm_bound +#check HighDimProb.BoundedOperatorNorm_rankOneRandomMatrix_of_sqNorm_bound +#check HighDimProb.PointwiseOperatorNormBound_rankOneRandomMatrix_of_sqNorm_bound #check HighDimProb.BoundedOperatorNorm_centered_of_bound_expect_bound #check HighDimProb.PointwiseOperatorNormBound_centered_of_bound_expect_bound #check HighDimProb.PointwiseOperatorNormBound_centered_of_bound_expect_bound_same @@ -26,7 +26,7 @@ example {Omega : Type*} [MeasurableSpace Omega] example {n : Nat} (v : Fin n -> Real) : HighDimProb.deterministicOperatorNorm - (fun i j : Fin n => v i * v j) <= HighDimProb.vectorSqNorm v := by + (HighDimProb.rankOneMatrix v) <= HighDimProb.vectorSqNorm v := by exact HighDimProb.rankOneOperatorNorm_le_vectorSqNorm v example {m n : Nat} (A B : Matrix (Fin m) (Fin n) Real) : @@ -36,11 +36,10 @@ example {m n : Nat} (A B : Matrix (Fin m) (Fin n) Real) : example {Omega : Type*} [MeasurableSpace Omega] {I : Type*} {n : Nat} (X : I -> Omega -> Fin n -> Real) (R : Real) - (hR : 0 <= R) (hX : forall i omega, HighDimProb.vectorSqNorm (X i omega) <= R) : HighDimProb.PointwiseOperatorNormBound - (fun i omega a b => X i omega a * X i omega b) R := by - exact HighDimProb.PointwiseOperatorNormBound_rankOne_of_sqNorm_bound X R hR hX + (fun i => HighDimProb.rankOneRandomMatrix (X i)) R := by + exact HighDimProb.PointwiseOperatorNormBound_rankOneRandomMatrix_of_sqNorm_bound X R hX example {Omega : Type*} [MeasurableSpace Omega] {I : Type*} {m n : Nat} (P : MeasureTheory.Measure Omega) (X : I -> HighDimProb.RandomMatrix Omega m n) diff --git a/HighDimProbTest/ExamplesAPI.lean b/HighDimProbTest/ExamplesAPI.lean index beb293e..392f07a 100644 --- a/HighDimProbTest/ExamplesAPI.lean +++ b/HighDimProbTest/ExamplesAPI.lean @@ -22,7 +22,7 @@ variable {rankOneN : Nat} variable (rankOneV : RankOneVector rankOneN) #check (rankOneOperatorNorm_le_vectorSqNorm rankOneV : - deterministicOperatorNorm (rankOneOuter rankOneV) <= vectorSqNorm rankOneV) + deterministicOperatorNorm (rankOneMatrix rankOneV) <= vectorSqNorm rankOneV) variable {kernelN : Nat} variable (kernelA : Matrix (Fin (kernelN + 1)) (Fin (kernelN + 1)) Real) diff --git a/HighDimProbTest/RandomMatrixAssumptionsAPI.lean b/HighDimProbTest/RandomMatrixAssumptionsAPI.lean index 7da526e..7d9d973 100644 --- a/HighDimProbTest/RandomMatrixAssumptionsAPI.lean +++ b/HighDimProbTest/RandomMatrixAssumptionsAPI.lean @@ -18,8 +18,8 @@ variable (K R : Real) #check IsotropicRowsSecondMoment #check IsotropicRowsCovariance #check CenteredEntries -#check BoundedOperatorNorm_rankOne_of_sqNorm_bound -#check PointwiseOperatorNormBound_rankOne_of_sqNorm_bound +#check BoundedOperatorNorm_rankOneRandomMatrix_of_sqNorm_bound +#check PointwiseOperatorNormBound_rankOneRandomMatrix_of_sqNorm_bound #check BoundedOperatorNorm_centered_of_bound_expect_bound #check PointwiseOperatorNormBound_centered_of_bound_expect_bound #check PointwiseOperatorNormBound_centered_of_bound_expect_bound_same @@ -30,12 +30,11 @@ variable (K R : Real) #check (IsotropicRowsSecondMoment P A : Prop) #check (IsotropicRowsCovariance P A : Prop) #check (CenteredEntries P A : Prop) -#check (PointwiseOperatorNormBound_rankOne_of_sqNorm_bound +#check (PointwiseOperatorNormBound_rankOneRandomMatrix_of_sqNorm_bound (X := X) (R := R) : - 0 <= R -> (forall i omega, vectorSqNorm (X i omega) <= R) -> PointwiseOperatorNormBound - (fun i omega a b => X i omega a * X i omega b) R) + (fun i => rankOneRandomMatrix (X i)) R) #check (BoundedOperatorNorm_centered_of_bound_expect_bound (P := P) (X := A) (R := R) (Rexp := K) : BoundedOperatorNorm A R -> diff --git a/HighDimProbTest/RandomMatrixBasicAPI.lean b/HighDimProbTest/RandomMatrixBasicAPI.lean index 5b12a14..c2c5d32 100644 --- a/HighDimProbTest/RandomMatrixBasicAPI.lean +++ b/HighDimProbTest/RandomMatrixBasicAPI.lean @@ -8,6 +8,7 @@ variable {P : Measure Omega} [IsProbabilityMeasure P] variable {m n : Nat} variable (A : RandomMatrix Omega m n) variable (X : RandomVector Omega n) +variable (x : Fin n -> Real) variable (i : Fin m) (j : Fin n) variable (a b : Fin n) variable (hA : IsRandomMatrix P A) @@ -17,6 +18,8 @@ variable (hX : IsRandomVector P X) #check matrixEntry #check IsRandomMatrix #check matrixEntry_apply +#check rankOneMatrix +#check rankOneMatrix_apply #check rankOneRandomMatrix #check rankOneRandomMatrix_apply #check matrixEntry_rankOneRandomMatrix @@ -26,6 +29,9 @@ variable (hX : IsRandomVector P X) #check measurable_randomMatrix_of_isRandomMatrix #check (matrixEntry A i j : RealRandomVariable Omega) +#check (rankOneMatrix x : Matrix (Fin n) (Fin n) Real) +#check (rankOneMatrix_apply x : forall a b, + rankOneMatrix x a b = x a * x b) #check (rankOneRandomMatrix X : RandomMatrix Omega n n) #check (rankOneRandomMatrix_apply X : forall omega a b, rankOneRandomMatrix X omega a b = X omega a * X omega b) diff --git a/HighDimProbTest/RandomMatrixOperatorNormAPI.lean b/HighDimProbTest/RandomMatrixOperatorNormAPI.lean index 8df975d..d29b8bd 100644 --- a/HighDimProbTest/RandomMatrixOperatorNormAPI.lean +++ b/HighDimProbTest/RandomMatrixOperatorNormAPI.lean @@ -35,6 +35,8 @@ variable (hA : IsRandomMatrix P A) #check deterministicOperatorNorm #check deterministicOperatorNorm_apply #check deterministicOperatorNorm_sub_le_add +#check rankOneMatrix +#check rankOneMatrix_apply #check rankOneOperatorNorm_le_vectorSqNorm #check matVecSqNorm #check matVecSqNorm_apply @@ -69,7 +71,7 @@ variable (hA : IsRandomMatrix P A) #check (deterministicOperatorNorm_sub_le_add M M : deterministicOperatorNorm (M - M) <= deterministicOperatorNorm M + deterministicOperatorNorm M) #check (rankOneOperatorNorm_le_vectorSqNorm v : - deterministicOperatorNorm (fun i j : Fin n => v i * v j) <= vectorSqNorm v) + deterministicOperatorNorm (rankOneMatrix v) <= vectorSqNorm v) #check (matVecSqNorm M x : Real) #check (randomMatVecSqNorm A x : RealRandomVariable Omega) #check (sqNorm_matVec_eq_matVecSqNorm A x : forall omega, sqNorm (matVec A x) omega = matVecSqNorm (A omega) x) @@ -86,12 +88,11 @@ variable (hA : IsRandomMatrix P A) #check (operatorNorm_le_of_operatorNormBoundSqStatement M L : Prop) #check (operatorNormBoundSq_of_operatorNorm_leStatement M L : Prop) #check (operatorNormMeasurabilityStatement P A : Prop) -#check (PointwiseOperatorNormBound_rankOne_of_sqNorm_bound +#check (PointwiseOperatorNormBound_rankOneRandomMatrix_of_sqNorm_bound (X := X) (R := L) : - 0 <= L -> (forall i omega, vectorSqNorm (X i omega) <= L) -> PointwiseOperatorNormBound - (fun i omega a b => X i omega a * X i omega b) L) + (fun i => rankOneRandomMatrix (X i)) L) #check (matrixQuadraticForm_sub T S x : matrixQuadraticForm (T - S) x = matrixQuadraticForm T x - matrixQuadraticForm S x) #check (quadraticForm_le_of_matrixLE (A := S) (B := T) : MatrixLE S T -> forall x, matrixQuadraticForm S x <= matrixQuadraticForm T x) diff --git a/docs/AbstractionLog.md b/docs/AbstractionLog.md index 25bcf9d..431c66b 100644 --- a/docs/AbstractionLog.md +++ b/docs/AbstractionLog.md @@ -1202,15 +1202,15 @@ ## RM rank-one operator-norm boundedness bridge -- Concrete version chosen: prove the rank-one self-outer-product bound directly - against `deterministicOperatorNorm` instead of introducing a new rank-one - matrix object or changing the matrix norm convention. +- Concrete version chosen: expose the self-outer product as the named + `rankOneMatrix` / `rankOneRandomMatrix` vocabulary while keeping the existing + `deterministicOperatorNorm` convention. - Proof-pattern decision: view `v vᵀ` as the linear map `x ↦ v` and use Cauchy--Schwarz plus `ContinuousLinearMap.opNorm_le_bound` under Mathlib's scoped L2 operator norm. - Assumption decision: the random wrappers consume an explicit pointwise - `vectorSqNorm <= R` hypothesis and keep the nonnegative-radius argument - visible, rather than inferring expectation or centered bounds. + `vectorSqNorm <= R` hypothesis without a separate `0 <= R` parameter; they do + not infer expectation or centered bounds. - Comment/source decision: Lean comments include public operator-norm and outer product URLs so readers can verify the mathematical formula. - Future upgrade path: next add the centered operator-norm triangle wrapper; diff --git a/docs/BookProgress.md b/docs/BookProgress.md index 5563dbc..e4e384c 100644 --- a/docs/BookProgress.md +++ b/docs/BookProgress.md @@ -981,8 +981,8 @@ is proved: ```lean rankOneOperatorNorm_le_vectorSqNorm -BoundedOperatorNorm_rankOne_of_sqNorm_bound -PointwiseOperatorNormBound_rankOne_of_sqNorm_bound +BoundedOperatorNorm_rankOneRandomMatrix_of_sqNorm_bound +PointwiseOperatorNormBound_rankOneRandomMatrix_of_sqNorm_bound ``` The deterministic lemma proves the finite-dimensional bound diff --git a/docs/RandomMatrixAPI.md b/docs/RandomMatrixAPI.md index c4fded4..e74f069 100644 --- a/docs/RandomMatrixAPI.md +++ b/docs/RandomMatrixAPI.md @@ -41,8 +41,8 @@ mainline. It is documentation only; theorem status is not upgraded here. - Lambda-max/operator-norm Matrix Bernstein tail theorem remains unproved. - Proved rank-one operator-norm prerequisite bridge: `rankOneOperatorNorm_le_vectorSqNorm`, - `BoundedOperatorNorm_rankOne_of_sqNorm_bound`, and - `PointwiseOperatorNormBound_rankOne_of_sqNorm_bound`. + `BoundedOperatorNorm_rankOneRandomMatrix_of_sqNorm_bound`, and + `PointwiseOperatorNormBound_rankOneRandomMatrix_of_sqNorm_bound`. - Proved centered operator-norm prerequisite bridge under an explicit expectation operator-norm bound: `deterministicOperatorNorm_sub_le_add`, @@ -66,8 +66,10 @@ mainline. It is documentation only; theorem status is not upgraded here. - `RandomMatrix`: abbrev, finite-dimensional real random matrix. - `matrixEntry`: def, entry random variable. - `IsRandomMatrix`: abbrev, entrywise measurability predicate. +- `rankOneMatrix`: def, deterministic rank-one self outer-product matrix. - `rankOneRandomMatrix`: def, vector-to-rank-one random matrix with entries `X_i * X_j`. +- `rankOneMatrix_apply`: theorem. - `rankOneRandomMatrix_apply`: theorem. - `matrixEntry_rankOneRandomMatrix`: theorem. - `isRandomMatrix_rankOneRandomMatrix`: theorem, entrywise measurability from @@ -158,14 +160,14 @@ mainline. It is documentation only; theorem status is not upgraded here. - `BoundedOperatorNorm`: def, pointwise operator-norm bound for one random matrix. -- `BoundedOperatorNorm_rankOne_of_sqNorm_bound`: theorem, rank-one pointwise - wrapper from vector squared-norm bounds. +- `BoundedOperatorNorm_rankOneRandomMatrix_of_sqNorm_bound`: theorem, rank-one + pointwise wrapper from vector squared-norm bounds. - `BoundedOperatorNorm_centered_of_bound_expect_bound`: theorem, centered wrapper from a pointwise bound plus an explicit expectation operator-norm bound. - `PointwiseOperatorNormBound`: def, indexed pointwise operator-norm bound. -- `PointwiseOperatorNormBound_rankOne_of_sqNorm_bound`: theorem, indexed - rank-one wrapper from vector squared-norm bounds. +- `PointwiseOperatorNormBound_rankOneRandomMatrix_of_sqNorm_bound`: theorem, + indexed rank-one wrapper from vector squared-norm bounds. - `PointwiseOperatorNormBound_centered_of_bound_expect_bound`: theorem, indexed centered wrapper with explicit expectation bound. - `PointwiseOperatorNormBound_centered_of_bound_expect_bound_same`: theorem, diff --git a/docs/Status.md b/docs/Status.md index 3032e89..e6c9ef4 100644 --- a/docs/Status.md +++ b/docs/Status.md @@ -23,8 +23,8 @@ bridge `deterministicOperatorNorm_sub_le_add`, `BoundedOperatorNorm_centered_of_bound_expect_bound`, `PointwiseOperatorNormBound_centered_of_bound_expect_bound`, the earlier rank-one operator-norm bridge `rankOneOperatorNorm_le_vectorSqNorm`, -`BoundedOperatorNorm_rankOne_of_sqNorm_bound`, and -`PointwiseOperatorNormBound_rankOne_of_sqNorm_bound`. The new vector-to-matrix +`BoundedOperatorNorm_rankOneRandomMatrix_of_sqNorm_bound`, and +`PointwiseOperatorNormBound_rankOneRandomMatrix_of_sqNorm_bound`. The new vector-to-matrix bridge proves entrywise measurability from `IsRandomVector`; entrywise integrability is proved only from explicit product-integrability assumptions or explicit coordinate `MemLp ... 2` assumptions. The new PSD nullspace bridge diff --git a/docs/TODO.md b/docs/TODO.md index f5c3ed3..254e015 100644 --- a/docs/TODO.md +++ b/docs/TODO.md @@ -14,8 +14,8 @@ `matrixBernsteinQuadraticFormUpperTailOptimizedScalarRHSWithBernsteinCoeff_under_primitives`. - Done: rank-one operator-norm prerequisite slice added `rankOneOperatorNorm_le_vectorSqNorm`, - `BoundedOperatorNorm_rankOne_of_sqNorm_bound`, and - `PointwiseOperatorNormBound_rankOne_of_sqNorm_bound`. + `BoundedOperatorNorm_rankOneRandomMatrix_of_sqNorm_bound`, and + `PointwiseOperatorNormBound_rankOneRandomMatrix_of_sqNorm_bound`. - Done: centered operator-norm prerequisite slice added `deterministicOperatorNorm_sub_le_add`, `BoundedOperatorNorm_centered_of_bound_expect_bound`, diff --git a/docs/TermMap.md b/docs/TermMap.md index 0d7963a..3479506 100644 --- a/docs/TermMap.md +++ b/docs/TermMap.md @@ -130,8 +130,8 @@ Note: some declarations exist as scaffolds, but the corresponding concept is not | Matrix-vector squared norm | Operator-norm bridge prerequisites | Squared Euclidean norm of `A x` using explicit matrix-vector finite sums. | `Finset.univ.sum`, `matVec` normal form, `Matrix.mulVec`, `EuclideanSpace` L2 norm | `matVecSqNorm`, `randomMatVecSqNorm`, `sqNorm_matVec_eq_matVecSqNorm`, `isRealRandomVariable_randomMatVecSqNorm`, `matVecSqNorm_eq_norm_sq_toLp_mulVec`, `norm_sq_toLp_mulVec_eq_matVecSqNorm` | `HighDimProb/RandomMatrix/OperatorNorm.lean` | implemented/proven experimental API | Provides a theorem-friendly finite-sum normal form and an exact bridge to the Mathlib L2 norm of `A x`. | | Squared operator-norm bound predicate | Matrix concentration prerequisites | Pointwise squared matrix-vector bound over all explicit unit vectors. | `IsUnitVector`, `matVecSqNorm`, `Matrix.Norms.L2Operator` | `OperatorNormBoundSq`, `RandomOperatorNormBoundSq`, `matVecSqNorm_le_of_operatorNormBoundSq`, `operatorNorm_le_of_operatorNormBoundSq`, `operatorNormBoundSq_of_operatorNorm_le` | `HighDimProb/RandomMatrix/OperatorNorm.lean` | implemented/proven experimental API | The explicit predicate is retained for theorem statements and is now bridged in both directions with `deterministicOperatorNorm` under the visible nonnegative-scale hypotheses. | | Exact operator-norm bridge targets | Matrix concentration prerequisites | Typed targets and proved bridges connecting explicit squared unit-vector bounds to Mathlib's scoped L2 matrix norm and measurability. | `Matrix.Norms.L2Operator`, product measurable spaces, `measurable_norm` | `operatorNorm_le_of_operatorNormBoundSqStatement`, `operatorNormBoundSq_of_operatorNorm_leStatement`, `operatorNormMeasurabilityStatement`, `operatorNorm_le_of_operatorNormBoundSq`, `operatorNormBoundSq_of_operatorNorm_le`, `instOpensMeasurableSpaceMatrixL2Operator`, `isRealRandomVariable_operatorNorm` | `HighDimProb/RandomMatrix/OperatorNorm.lean` | proven bridge plus typed-prop compatibility targets | Stage MC2-fix proves the exact comparison directions and operator-norm measurability; the statement-only targets remain as API signposts. | -| Rank-one operator-norm bound | Rank-one covariance and matrix-concentration prerequisites | The self-outer product `v vᵀ` has induced L2 operator norm bounded by `||v||₂²`. | `Matrix.Norms.L2Operator`, `ContinuousLinearMap.opNorm_le_bound`, Cauchy-Schwarz | `rankOneOperatorNorm_le_vectorSqNorm` | `HighDimProb/RandomMatrix/OperatorNorm.lean` | proven experimental API | The proof uses the existing `deterministicOperatorNorm` convention and does not introduce new rank-one vocabulary. | -| Rank-one pointwise operator-norm bound | Matrix Bernstein boundedness prerequisites | A pointwise squared-vector-norm bound implies a pointwise operator-norm bound for `omega |-> X omega X omegaᵀ` and indexed families. | `operatorNorm`, `vectorSqNorm`, `PointwiseOperatorNormBound` | `BoundedOperatorNorm_rankOne_of_sqNorm_bound`, `PointwiseOperatorNormBound_rankOne_of_sqNorm_bound` | `HighDimProb/RandomMatrix/Assumptions.lean` | proven experimental API | This is a boundedness bridge only; centered expectation bounds, measurability/integrability bridges, and PSD nullspace converse are handled as separate tasks. | +| Rank-one operator-norm bound | Rank-one covariance and matrix-concentration prerequisites | The named self-outer product `rankOneMatrix v` has induced L2 operator norm bounded by `||v||₂²`. | `rankOneMatrix`, `Matrix.Norms.L2Operator`, `ContinuousLinearMap.opNorm_le_bound`, Cauchy-Schwarz | `rankOneOperatorNorm_le_vectorSqNorm` | `HighDimProb/RandomMatrix/OperatorNorm.lean` | proven experimental API | The proof uses the existing `deterministicOperatorNorm` convention while keeping the rank-one matrix object named. | +| Rank-one pointwise operator-norm bound | Matrix Bernstein boundedness prerequisites | A pointwise squared-vector-norm bound implies a pointwise operator-norm bound for `rankOneRandomMatrix X` and indexed families. | `operatorNorm`, `rankOneRandomMatrix`, `vectorSqNorm`, `PointwiseOperatorNormBound` | `BoundedOperatorNorm_rankOneRandomMatrix_of_sqNorm_bound`, `PointwiseOperatorNormBound_rankOneRandomMatrix_of_sqNorm_bound` | `HighDimProb/RandomMatrix/Assumptions.lean` | proven experimental API | This is a boundedness bridge only; centered expectation bounds, measurability/integrability bridges, and PSD nullspace converse are handled as separate tasks. | | Centered operator-norm bound | Matrix Bernstein boundedness prerequisites | Centering satisfies `||X(ω) - E X||op <= ||X(ω)||op + ||E X||op`; a pointwise bound plus explicit expectation bound yields a bound on `centeredRandomMatrix`. | `norm_sub_le`, `matrixExpect`, `centeredRandomMatrix`, `PointwiseOperatorNormBound` | `deterministicOperatorNorm_sub_le_add`, `BoundedOperatorNorm_centered_of_bound_expect_bound`, `PointwiseOperatorNormBound_centered_of_bound_expect_bound`, `PointwiseOperatorNormBound_centered_of_bound_expect_bound_same` | `HighDimProb/RandomMatrix/OperatorNorm.lean`, `HighDimProb/RandomMatrix/Assumptions.lean` | proven experimental API | Algebraic explicit-bound wrapper only; it does not prove entrywise integrability, vector-to-rank-one measurability, or expectation operator-norm contraction. | | PSD nullspace converse | Matrix Bernstein covariance-style prerequisites | For a real PSD matrix, a zero quadratic form `xᵀ A x = 0` is equivalent to `A x = 0`; HighDimProb exposes both Mathlib `Matrix.PosSemidef` and explicit `IsPSDMatrix` variants. | `Matrix.PosSemidef.dotProduct_mulVec_zero_iff`, `matrixQuadraticForm`, `Matrix.mulVec`, `IsPSDMatrix` | `posSemidef_of_isPSDMatrix`, `matrixQuadraticForm_eq_zero_iff_mulVec_eq_zero_of_posSemidef`, `matrix_mulVec_eq_zero_of_posSemidef_quadraticForm_eq_zero`, `matrixQuadraticForm_eq_zero_iff_mulVec_eq_zero_of_isPSDMatrix`, `matrix_mulVec_eq_zero_of_isPSDMatrix_quadraticForm_eq_zero` | `HighDimProb/RandomMatrix/Spectral.lean`, `HighDimProb/Examples/RandomMatrix/KernelNullspaceUsage.lean` | proven experimental API | This is a deterministic PSD kernel bridge only; it does not prove expectation contraction or Matrix Bernstein tails. | | Matrix symmetry/self-adjointness | Matrix Bernstein prerequisites | Pointwise real symmetric/self-adjoint matrix predicates and random-matrix wrappers. | `Matrix.IsSymm`, `Matrix.IsHermitian` | `IsSymmetricMatrix`, `IsSelfAdjointMatrix`, `RandomSymmetricMatrix`, `RandomSelfAdjointMatrix` | `HighDimProb/RandomMatrix/SelfAdjoint.lean` | implemented experimental API | Stage MC1 keeps the vocabulary explicit and does not prove spectral theorems. |