Skip to content

Add centered operator norm boundedness bridge#9

Merged
dududuguo merged 1 commit into
mainfrom
rm-centered-operator-norm-bound
Jun 13, 2026
Merged

Add centered operator norm boundedness bridge#9
dududuguo merged 1 commit into
mainfrom
rm-centered-operator-norm-bound

Conversation

@freezed-corpse-143

Copy link
Copy Markdown
Collaborator

Summary

  • Add an explicit centered random-matrix operator-norm bound bridge.
  • Expose deterministicOperatorNorm_sub_le_add from the deterministic operator-norm API.
  • Add BoundedOperatorNorm / PointwiseOperatorNormBound wrappers for centeredRandomMatrix using an explicit bound on matrixExpect P X.
  • Update focused API tests, judge checks, and Matrix Bernstein prerequisite documentation.

Motivation

This is the next small prerequisite after the rank-one operator-norm bound bridge. Matrix Bernstein setup often needs a centered summand bound, but this PR intentionally keeps the result algebraic and explicit: it uses the triangle inequality and a supplied expectation-norm bound, without proving expectation contraction or vector-to-matrix integrability.

Scope

  • Lean API:
    • HighDimProb.RandomMatrix.OperatorNorm
    • HighDimProb.RandomMatrix.Assumptions
  • Tests / judge:
    • RandomMatrix operator norm / assumptions / concentration API tests
    • HighDimProbJudge.RandomMatrix.OperatorNormUse
  • Docs:
    • Status, TODO, TermMap, BookProgress, AbstractionLog, TheoremAtlas, and Matrix Bernstein/concentration planning docs

This PR does not prove:

  • expectation contraction for matrixExpect
  • vector-to-rank-one measurability or integrability
  • PSD nullspace converse
  • a completed Matrix Bernstein tail theorem

Stacking

This PR is intended to be stacked on #8 (rm-rank-one-operator-norm-bound) so the review diff contains only the centered operator-norm increment. After #8 lands, this PR can be retargeted to main if needed.

Review gates

  • Code Review: completed locally; no blocking issues after comment/docs boundary clarification.
  • Format Review: git diff --check passed.
  • Git Review: tracked diff only; local/generated files are excluded.
  • Comment Review: new Lean comments include public reference URLs and explicitly state the non-goals.

Testing

  • refined forbidden-token scan over HighDimProb, HighDimProbTest, HighDimProbJudge
  • conflict-marker scan
  • git diff --check
  • lake build
  • lake test
  • lake build HighDimProbJudge
  • python scripts/judge_policy_check.py

Expose the centered random-matrix bound as a small algebraic wrapper around the deterministic operator-norm triangle inequality, while keeping the stronger analytic obligations out of scope.

Constraint: stacked on PR #8 because the centered bridge reuses the rank-one operator-norm API branch as its clean base.
Rejected: proving expectation contraction or measurability/integrability here | those are separate next safe tasks and would broaden the review surface.
Confidence: high
Scope-risk: narrow
Directive: Keep this PR framed as explicit-bound algebra only; do not present it as a full centered Matrix Bernstein prerequisite closure.
Tested: lake build; lake test; lake build HighDimProbJudge; python scripts/judge_policy_check.py; git diff --check; forbidden-token and conflict-marker scans
Not-tested: GitHub PR CI, because the branch has not been pushed or opened in this local preparation step.
@dududuguo dududuguo changed the base branch from rm-rank-one-operator-norm-bound to main June 13, 2026 13:13
@dududuguo dududuguo merged commit 1b52170 into main Jun 13, 2026
4 checks passed
@dududuguo dududuguo deleted the rm-centered-operator-norm-bound branch June 13, 2026 13:46
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants