Advance provider-backed Lieb theorem surfaces#32
Closed
freezed-corpse-143 wants to merge 1 commit into
Closed
Conversation
Port the provider-backed log-order, Epstein-conditional, and integrability compression surfaces into the main RandomMatrix lane while keeping the remaining theorem assumptions explicit. Constraint: Provider already depends on HighDimProb, so theorem content is ingested into the main repo instead of adding a reverse Lake dependency. Rejected: Claiming unconditional Lieb/Epstein/Matrix Bernstein closure | Epstein affine-line concavity, independence, conditional expectation, variance proxy, and full-sum trace integrability remain explicit frontiers. Confidence: high Scope-risk: moderate Directive: Keep provider-backed wrappers assumption-explicit; do not weaken theorem-boundary honesty by renaming conditional leaves as unconditional Tropp/Lieb results. Tested: git diff --check; python .github/scripts/check_text_quality.py; python scripts/judge_policy_check.py; lake build HighDimProb.RandomMatrix.LiebProvider HighDimProb.RandomMatrix.ConcentrationStatements HighDimProbTest.RandomMatrixLiebProviderAPI HighDimProbJudge.RandomMatrix.LiebProviderUse; lake test; lake build; lake build HighDimProbJudge Not-tested: GitHub CI has not run before PR creation.
10 tasks
Owner
|
Thanks for pushing the provider-backed Lieb theorem surfaces forward. The useful pieces from this PR have been manually integrated and refactored into main in 7413583 (Integrate Lieb provider bridge layer), including the provider-facing imports, Epstein-conditional route, log/order wrappers, bounded integrability providers, tests, judge surface, and docs. I'm closing this PR instead of merging the old branch because the final main version deliberately keeps the remaining Epstein/Lieb, independence, conditional-expectation, variance-proxy, and full Matrix Bernstein frontiers explicit. |
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
Motivation
The provider repository now contains enough deterministic log-order, trace monotonicity, Epstein-conditional, and bounded-integrability material to advance the main theorem roadmap. This PR ingests those facts into HighDimProb while keeping open theorem frontiers explicit.
Scope
HighDimProb.RandomMatrix.LiebProviderand supporting provider-port modules.ConcentrationStatementswithMatrixBernsteinConditioningTraceMGFProviderAssumptionsand a tail wrapper.EpsteinAffineLineConcavity, independence, conditional expectation, variance proxy, and full-sum trace integrability as explicit assumptions.Testing
git diff --checkpython .github/scripts/check_text_quality.pypython scripts/judge_policy_check.pylake build HighDimProb.RandomMatrix.LiebProvider HighDimProb.RandomMatrix.ConcentrationStatements HighDimProbTest.RandomMatrixLiebProviderAPI HighDimProbJudge.RandomMatrix.LiebProviderUselake testlake buildlake build HighDimProbJudgeNotes