Add PSD nullspace converse bridge#11
Merged
Merged
Conversation
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.
dududuguo
changed the base branch from
rm-vector-to-matrix-measurability-integrability
to
main
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
HighDimProb.RandomMatrix.Spectral:posSemidef_of_isPSDMatrixmatrixQuadraticForm_eq_zero_iff_mulVec_eq_zero_of_posSemidefmatrix_mulVec_eq_zero_of_posSemidef_quadraticForm_eq_zeromatrixQuadraticForm_eq_zero_iff_mulVec_eq_zero_of_isPSDMatrixmatrix_mulVec_eq_zero_of_isPSDMatrix_quadraticForm_eq_zeroKernelNullspaceUsageexamples through the new core bridge.Motivation
This closes the narrow PSD nullspace converse prerequisite for covariance-style RandomMatrix examples: for a PSD matrix, a zero quadratic form identifies a kernel/invisible direction.
Scope
rm-vector-to-matrix-measurability-integrability).Testing
lake buildlake testlake build HighDimProbJudgepython scripts/judge_policy_check.pygit diff --checkNext safe task
RM-expectation-contraction