diff --git a/HighDimProb/RandomMatrix/CStarBridge.lean b/HighDimProb/RandomMatrix/CStarBridge.lean index 30f3f21..f84aaf2 100644 --- a/HighDimProb/RandomMatrix/CStarBridge.lean +++ b/HighDimProb/RandomMatrix/CStarBridge.lean @@ -77,6 +77,43 @@ theorem isSelfAdjoint_realMatrixToCStarMatrix {n : Nat} simpa using h.symm simp [realMatrixToCStarMatrix, hsym] +/-! ## Proved transport from explicit complexified premises -/ + +/-- Nonnegativity of the complexified matrix survives the `CStarMatrix` representation. + +This is deliberately stated with the complexified matrix premise. The separate +real-to-complex positivity bridge is not claimed here. -/ +theorem realMatrixToCStarMatrix_nonneg_of_complexified_nonneg {n : Nat} + (A : Matrix (Fin n) (Fin n) Real) + (hA : 0 <= A.map (algebraMap Real Complex)) : + 0 <= realMatrixToCStarMatrix A := by + exact map_rel (CStarMatrix.ofMatrixStarAlgEquiv : + Matrix (Fin n) (Fin n) Complex ≃⋆ₐ[Complex] + CStarMatrix (Fin n) (Fin n) Complex) hA + +/-- Loewner order of complexified matrices survives the `CStarMatrix` representation. + +This is the proved CStar-side order transport contract. It does not by itself +prove that a HighDimProb `MatrixLE A B` supplies the complexified order premise. -/ +theorem realMatrixToCStarMatrixLE_of_complexified_le {n : Nat} + (A B : Matrix (Fin n) (Fin n) Real) + (hAB : A.map (algebraMap Real Complex) <= B.map (algebraMap Real Complex)) : + realMatrixToCStarMatrix A <= realMatrixToCStarMatrix B := by + exact map_rel (CStarMatrix.ofMatrixStarAlgEquiv : + Matrix (Fin n) (Fin n) Complex ≃⋆ₐ[Complex] + CStarMatrix (Fin n) (Fin n) Complex) hAB + +/-- Strict positivity of the complexified matrix survives the `CStarMatrix` representation. -/ +theorem realMatrixToCStarStrictlyPositive_of_complexified {n : Nat} + (A : Matrix (Fin n) (Fin n) Real) + (hA : IsStrictlyPositive (A.map (algebraMap Real Complex))) : + IsStrictlyPositive (realMatrixToCStarMatrix A) := by + refine ⟨?_, ?_⟩ + · exact realMatrixToCStarMatrix_nonneg_of_complexified_nonneg A hA.nonneg + · exact IsUnit.map (CStarMatrix.ofMatrixStarAlgEquiv : + Matrix (Fin n) (Fin n) Complex ≃⋆ₐ[Complex] + CStarMatrix (Fin n) (Fin n) Complex) hA.isUnit + /-! ## Statement targets for the remaining transport layer -/ /-- Target: strict positivity survives the real-to-CStar representation. -/ @@ -95,6 +132,17 @@ abbrev realMatrixToCStarLogBack_statement {n : Nat} CFC.log (realMatrixToCStarMatrix A) = realMatrixToCStarMatrix (CFC.log A) +/-- Close the log-back statement when the log transport equality is supplied explicitly. + +This wrapper is intentionally an assumption consumer, not a proof of CFC-log +compatibility for real-to-CStar transport. -/ +theorem realMatrixToCStarLogBack_of_transport {n : Nat} + (A : Matrix (Fin n) (Fin n) Real) + (hlog : CFC.log (realMatrixToCStarMatrix A) = + realMatrixToCStarMatrix (CFC.log A)) : + realMatrixToCStarLogBack_statement A := + hlog + end end HighDimProb diff --git a/HighDimProbJudge/RandomMatrix/TraceExpUse.lean b/HighDimProbJudge/RandomMatrix/TraceExpUse.lean index 9ec86ef..ceb2d42 100644 --- a/HighDimProbJudge/RandomMatrix/TraceExpUse.lean +++ b/HighDimProbJudge/RandomMatrix/TraceExpUse.lean @@ -2,7 +2,7 @@ import HighDimProb.RandomMatrix noncomputable section -open scoped MatrixOrder Matrix.Norms.Operator +open scoped ComplexOrder MatrixOrder Matrix.Norms.Operator #check HighDimProb.matrixExp #check HighDimProb.matrixTrace @@ -103,6 +103,32 @@ open scoped MatrixOrder Matrix.Norms.Operator #check HighDimProb.realMatrixToCStarStrictlyPositive_statement #check HighDimProb.realMatrixToCStarMatrixLE_statement #check HighDimProb.realMatrixToCStarLogBack_statement +#check HighDimProb.realMatrixToCStarMatrix_nonneg_of_complexified_nonneg +#check HighDimProb.realMatrixToCStarMatrixLE_of_complexified_le +#check HighDimProb.realMatrixToCStarStrictlyPositive_of_complexified +#check HighDimProb.realMatrixToCStarLogBack_of_transport + +example {n : Nat} (A : Matrix (Fin n) (Fin n) Real) + (hA : 0 <= A.map (algebraMap Real Complex)) : + 0 <= HighDimProb.realMatrixToCStarMatrix A := + HighDimProb.realMatrixToCStarMatrix_nonneg_of_complexified_nonneg A hA + +example {n : Nat} (A B : Matrix (Fin n) (Fin n) Real) + (hAB : A.map (algebraMap Real Complex) <= B.map (algebraMap Real Complex)) : + HighDimProb.realMatrixToCStarMatrix A <= HighDimProb.realMatrixToCStarMatrix B := + HighDimProb.realMatrixToCStarMatrixLE_of_complexified_le A B hAB + +example {n : Nat} (A : Matrix (Fin n) (Fin n) Real) + (hA : IsStrictlyPositive (A.map (algebraMap Real Complex))) : + IsStrictlyPositive (HighDimProb.realMatrixToCStarMatrix A) := + HighDimProb.realMatrixToCStarStrictlyPositive_of_complexified A hA + +example {n : Nat} (A : Matrix (Fin n) (Fin n) Real) + (hlog : CFC.log (HighDimProb.realMatrixToCStarMatrix A) = + HighDimProb.realMatrixToCStarMatrix (CFC.log A)) : + HighDimProb.realMatrixToCStarLogBack_statement A := + HighDimProb.realMatrixToCStarLogBack_of_transport A hlog + #check HighDimProb.matrixExpLogDomainForSelfAdjoint_statement #check HighDimProb.matrixLog_le_of_le_matrixExp_statement #check HighDimProb.matrixLog_le_of_le_matrixExp diff --git a/HighDimProbTest/RandomMatrixCStarBridgeAPI.lean b/HighDimProbTest/RandomMatrixCStarBridgeAPI.lean new file mode 100644 index 0000000..1f07e91 --- /dev/null +++ b/HighDimProbTest/RandomMatrixCStarBridgeAPI.lean @@ -0,0 +1,41 @@ +import HighDimProb.RandomMatrix.CStarBridge + +open HighDimProb +open scoped ComplexOrder MatrixOrder Matrix.Norms.Operator + +variable {n : Nat} +variable (A B : Matrix (Fin n) (Fin n) Real) + +#check realMatrixToCStarMatrix +#check realMatrixToCStarMatrix_apply +#check realMatrixToCStarMatrix_add +#check realMatrixToCStarMatrix_sub +#check isSelfAdjoint_realMatrixToCStarMatrix +#check realMatrixToCStarMatrix_nonneg_of_complexified_nonneg +#check realMatrixToCStarMatrixLE_of_complexified_le +#check realMatrixToCStarStrictlyPositive_of_complexified +#check realMatrixToCStarStrictlyPositive_statement +#check realMatrixToCStarMatrixLE_statement +#check realMatrixToCStarLogBack_statement +#check realMatrixToCStarLogBack_of_transport + +example + (hA : 0 <= A.map (algebraMap Real Complex)) : + 0 <= realMatrixToCStarMatrix A := + realMatrixToCStarMatrix_nonneg_of_complexified_nonneg A hA + +example + (hAB : A.map (algebraMap Real Complex) <= B.map (algebraMap Real Complex)) : + realMatrixToCStarMatrix A <= realMatrixToCStarMatrix B := + realMatrixToCStarMatrixLE_of_complexified_le A B hAB + +example + (hA : IsStrictlyPositive (A.map (algebraMap Real Complex))) : + IsStrictlyPositive (realMatrixToCStarMatrix A) := + realMatrixToCStarStrictlyPositive_of_complexified A hA + +example + (hlog : CFC.log (realMatrixToCStarMatrix A) = + realMatrixToCStarMatrix (CFC.log A)) : + realMatrixToCStarLogBack_statement A := + realMatrixToCStarLogBack_of_transport A hlog diff --git a/HighDimProbTest/RandomMatrixHardboneStatementsAPI.lean b/HighDimProbTest/RandomMatrixHardboneStatementsAPI.lean index 715d869..707974c 100644 --- a/HighDimProbTest/RandomMatrixHardboneStatementsAPI.lean +++ b/HighDimProbTest/RandomMatrixHardboneStatementsAPI.lean @@ -3,7 +3,7 @@ import HighDimProb.RandomMatrix.HardboneStatements open MeasureTheory open HighDimProb -open scoped MatrixOrder Matrix.Norms.Operator +open scoped ComplexOrder MatrixOrder Matrix.Norms.Operator variable {Omega : Type*} [MeasurableSpace Omega] variable {P : Measure Omega} @@ -36,6 +36,10 @@ variable (mHist : Fin m -> MeasurableSpace Omega) #check realMatrixToCStarStrictlyPositive_statement #check realMatrixToCStarMatrixLE_statement #check realMatrixToCStarLogBack_statement +#check realMatrixToCStarMatrix_nonneg_of_complexified_nonneg +#check realMatrixToCStarMatrixLE_of_complexified_le +#check realMatrixToCStarStrictlyPositive_of_complexified +#check realMatrixToCStarLogBack_of_transport #check traceMatrixExp_mono_add_selfAdjoint_statement #check troppLogExpComparisonToK_of_logOrderKChain_statement #check liebTraceExpConcavity_statement @@ -120,6 +124,27 @@ example : Prop := example : Prop := realMatrixToCStarLogBack_statement A +example + (hA : 0 <= A.map (algebraMap Real Complex)) : + 0 <= realMatrixToCStarMatrix A := + realMatrixToCStarMatrix_nonneg_of_complexified_nonneg A hA + +example + (hAB : M.map (algebraMap Real Complex) <= K.map (algebraMap Real Complex)) : + realMatrixToCStarMatrix M <= realMatrixToCStarMatrix K := + realMatrixToCStarMatrixLE_of_complexified_le M K hAB + +example + (hA : IsStrictlyPositive (A.map (algebraMap Real Complex))) : + IsStrictlyPositive (realMatrixToCStarMatrix A) := + realMatrixToCStarStrictlyPositive_of_complexified A hA + +example + (hlog : CFC.log (realMatrixToCStarMatrix A) = + realMatrixToCStarMatrix (CFC.log A)) : + realMatrixToCStarLogBack_statement A := + realMatrixToCStarLogBack_of_transport A hlog + example : Prop := troppMasterTraceMGFStep_of_liebJensen_statement (P := P) H Y diff --git a/docs/RandomMatrixAPI.md b/docs/RandomMatrixAPI.md index e521761..6b263a1 100644 --- a/docs/RandomMatrixAPI.md +++ b/docs/RandomMatrixAPI.md @@ -46,14 +46,20 @@ CStar representation bridge: - `realMatrixToCStarMatrix_add` - `realMatrixToCStarMatrix_sub` - `isSelfAdjoint_realMatrixToCStarMatrix` +- `realMatrixToCStarMatrix_nonneg_of_complexified_nonneg` +- `realMatrixToCStarMatrixLE_of_complexified_le` +- `realMatrixToCStarStrictlyPositive_of_complexified` - `realMatrixToCStarStrictlyPositive_statement` - `realMatrixToCStarMatrixLE_statement` - `realMatrixToCStarLogBack_statement` +- `realMatrixToCStarLogBack_of_transport` These expose the real-matrix to `CStarMatrix` representation layer needed to -reuse Mathlib CStar functional-calculus order results. Strict positivity, -Loewner-order, and `CFC.log` transport are still statement targets, not proved -facts. +reuse Mathlib CStar functional-calculus order results. The CStar-side transport +from explicit complexified nonnegativity, Loewner order, and strict positivity +premises is proved. The real-matrix-to-complexified positivity/order bridge and +unconditional `CFC.log` transport remain open; `realMatrixToCStarLogBack_of_transport` +only consumes an explicitly supplied log-back equality. ## Matrix Bernstein Surface @@ -194,7 +200,7 @@ Hardbone status table: | Scalar Bernstein hardbone leaf | `scalarBernsteinExpQuadraticInequality_statement` | proven by `scalarBernsteinExpQuadraticInequality` | CFC-chain assumptions can reuse the proved scalar theorem | none for this scalar leaf | | Bernstein CFC | `bernsteinMatrixExp_le_quadratic_statement` | proven by `bernsteinMatrixExp_le_quadratic` | `bernsteinMatrixExp_le_quadratic_of_cfcLeaves` documents the reusable composition | preferred `*_of_troppAssumptions` wrappers bypass pointwise CFC fields; explicit-CFC wrappers remain for compatibility | | Matrix log/order bridge | `matrixLog_le_of_le_matrixExp_statement` | proven by `matrixLog_le_of_le_matrixExp` | turns explicit log-monotonicity and `matrixExp` log-domain premises into `log M <= K` | `matrixExp` log-domain is supplied by `matrixExpLogDomainForSelfAdjoint`; operator-log monotonicity remains the external input | -| Real-to-CStar bridge | `realMatrixToCStarMatrix` and transport statement targets | basic representation map, add/sub, and self-adjoint transport proved | exposes the CStar representation route for future operator-log monotonicity proofs | strict positivity/order/log-back transport from real matrices to `CStarMatrix` remains open | +| Real-to-CStar bridge | `realMatrixToCStarMatrix` and transport statement targets | representation map, add/sub, self-adjoint transport, and CStar-side positivity/order/strict-positivity transport from explicit complexified premises proved | exposes the CStar representation route for future operator-log monotonicity proofs | real-to-complex positivity/order premises and unconditional log-back transport remain open | | Log/order-to-`K` | `troppLogExpComparisonToK_of_logOrderKChain_statement` | typed-prop | `troppLogExpComparisonToK_of_logMonotone_traceExpMono` | trace-exp monotonicity plus the explicit log/order bridge inputs | | Tropp/Lieb/GT one-step | `troppMasterTraceMGFStep_of_liebJensen_statement` | typed-prop | `troppMasterTraceMGFStep_of_liebJensen` | Lieb concavity, probability-measure Jensen, log-exp normalization; Golden-Thompson is separate | | Conditioning / independence | `troppConditionalStep_of_iIndepFun_statement` | proven by `troppConditionalStep_of_iIndepFun` | `troppMasterTraceMGFConditionalStep_of_conditioningBridge` | thin forwarder only; generated histories, history/current-step independence, finite-family independence, and conditional expectation reduction remain explicit premises | diff --git a/docs/Status.md b/docs/Status.md index 18e7884..43d2f00 100644 --- a/docs/Status.md +++ b/docs/Status.md @@ -360,8 +360,10 @@ Low-level prefix/state, reindex, negative-family, nullspace/decomposition, exact `RM-LIEB-S4-real-matrix-to-cstar-log-monotonicity-contract`, proving that Mathlib `CFC.log_le_log` is available on `CStarMatrix (Fin n) (Fin n) ℂ` while leaving real-matrix transport open. - Completed hardbone contract leaf: `RM-LIEB-S5-real-to-cstar-transport-api-contract`, proving the basic real-to-`CStarMatrix` transport shape in a probe, including entrywise, add/sub, and self-adjoint transport; positivity/order/log transport remains open. +- Completed hardbone contract leaf: + `RM-LIEB-S6-real-to-cstar-positivity-order-transport-contract`, proving the CStar-side transport from explicit complexified nonnegativity, Loewner-order, and strict-positivity premises. The real-to-complex positivity/order bridge and unconditional `CFC.log` log-back compatibility remain open. - Next safe hardbone task: - `RM-LIEB-S6-real-to-cstar-positivity-order-transport-contract`, focused on positivity/order/log transport for the real-to-CStar route. + `RM-LIEB-S7-real-to-complexified-positivity-order-bridge-audit-contract`, focused on whether HighDimProb real PSD/`MatrixLE`/strict-positivity facts can supply the complexified premises without overstating log-back compatibility. ## Verification diff --git a/docs/TODO.md b/docs/TODO.md index f2490f3..901d8aa 100644 --- a/docs/TODO.md +++ b/docs/TODO.md @@ -26,8 +26,12 @@ This is the active short list. Old completed task logs were collapsed into future provider compression; the compact bounded-row sample-covariance route remains the reader-facing surface. - Next RandomMatrix hardbone task: - `RM-LIEB-S6-real-to-cstar-positivity-order-transport-contract`. -- That next task should audit positivity/order/log transport for the real-to-CStar route; the basic transport map, entrywise behavior, add/sub, and self-adjoint transport are probe-ready. + `RM-LIEB-S7-real-to-complexified-positivity-order-bridge-audit-contract`. +- That next task should audit whether HighDimProb real PSD, `MatrixLE`, and real + strict-positivity assumptions can provide the complexified premises consumed + by the proved real-to-`CStarMatrix` transport lemmas. Do not treat `CFC.log` + log-back compatibility as proved unless a separate compatibility theorem is + established. ## Active Documentation Work diff --git a/docs/TestPlan.md b/docs/TestPlan.md index f70e397..2a1914c 100644 --- a/docs/TestPlan.md +++ b/docs/TestPlan.md @@ -38,8 +38,10 @@ git diff --check - RandomMatrix hardbone statement-target checks, including the proved Bernstein CFC hardbone leaf, the proved matrix-exp/log normalization and log-domain leaves, the proved matrix log/order bridge leaf, the proved excess-support trace bridge leaf, - and the proved centered-square expectation bridge leaf are covered in + the proved centered-square expectation bridge leaf, and the proved + real-to-`CStarMatrix` complexified positivity/order transport leaf are covered in `HighDimProbTest/RandomMatrixHardboneStatementsAPI.lean`, + `HighDimProbTest/RandomMatrixCStarBridgeAPI.lean`, and `HighDimProbJudge/RandomMatrix/TraceExpUse.lean`. - RandomMatrix sample-covariance negative-side provider-transfer adapters, the compact `SampleCovarianceTailTarget` / diff --git a/docs/TheoremAtlas.md b/docs/TheoremAtlas.md index 3e27782..5728dad 100644 --- a/docs/TheoremAtlas.md +++ b/docs/TheoremAtlas.md @@ -78,7 +78,7 @@ supplies it from coordinate `MemLp 4` assumptions via Mathlib Holder product APIs. The bounded-row provider `integrableRandomMatrix_randomMatrixSquare_rankOneRandomMatrix_of_sqNorm_bound_memLp_two` supplies it from coordinate `MemLp 2` plus pointwise `vectorSqNorm <= R`. -Centered rank-one square-integrability providers are proved for coordinate `MemLp 4` and bounded-row `MemLp 2` routes. The row-specific exact-row consumer `sampleCovarianceVarianceProxy_sharp_of_exactRowSqNorm_bound_memLp_two` now supplies a `rowSqNormVarianceProxyNormRHS R` variance-proxy bound from coordinate `MemLp 2`, pointwise `vectorSqNorm <= R_i`, nonnegative radii, and the explicit hardbone sharp-chain premise. The bridge layer connects generic centered-square chains to exact-row sample-covariance variance-proxy consumers, transfers exact-row control to the negative family, and exposes positive/two-sided exact-row centered-square wrappers and bundles. The deterministic PSD Loewner-to-operator-norm bridge is proved as `deterministicMatrixVarianceProxyNorm_mono_of_matrixLE`. These are infrastructure routes; full generic centered-square providers, Tropp/Lieb, trace-MGF integrability, and full Matrix Bernstein remain explicit or open. +Centered rank-one square-integrability providers are proved for coordinate `MemLp 4` and bounded-row `MemLp 2` routes. The row-specific exact-row consumer `sampleCovarianceVarianceProxy_sharp_of_exactRowSqNorm_bound_memLp_two` now supplies a `rowSqNormVarianceProxyNormRHS R` variance-proxy bound from coordinate `MemLp 2`, pointwise `vectorSqNorm <= R_i`, nonnegative radii, and the explicit hardbone sharp-chain premise. The bridge layer connects generic centered-square chains to exact-row sample-covariance variance-proxy consumers, transfers exact-row control to the negative family, and exposes positive/two-sided exact-row centered-square wrappers and bundles. The deterministic PSD Loewner-to-operator-norm bridge is proved as `deterministicMatrixVarianceProxyNorm_mono_of_matrixLE`. The real-to-`CStarMatrix` route now transports explicit complexified nonnegativity, Loewner order, and strict positivity premises to CStar order/strict positivity; real-to-complex positivity/order and unconditional `CFC.log` log-back compatibility remain separate blockers. These are infrastructure routes; full generic centered-square providers, Tropp/Lieb, trace-MGF integrability, and full Matrix Bernstein remain explicit or open. The rank/support trace-bound bridge is proved by `traceMatrixExp_le_trace_support_exp_lambdaMax_of_supportDomination`, with rank/support consumers for the hardbone targets. Deterministic trace/rank