feat(Channel/Schwarz): add matrix Bochner positivity lemma (#3462)

* feat(Channel/Schwarz): add matrix Bochner positivity lemma

* doc(operator-jensen): clarify available scalar inputs

* style(operator-jensen): rename matrix integral positivity lemma

---------

Co-authored-by: Sirui Lu <texra-ai@outlook.com>

Author: LionSR

TNLean/Axioms/OperatorConvexity.lean

@@ -65,16 +65,18 @@ The remaining Mathlib or local formalization gaps are:
   For the concave `rpow` case the per-resolvent core is already available in
   `TNLean.Channel.Schwarz.OperatorJensenAux` (`povm_resolvent_inv_le`); see the
   proof plan below.
-* Monotonicity of the matrix-valued Bochner integral in the Loewner order, and
-  pulling a positive linear map through that integral
-  (`ContinuousLinearMap.integral_comp_comm`): the analytic ingredients of the
-  integral route.  Concretely, the Loewner monotonicity step requires a closed
-  positive-semidefinite cone (`OrderClosedTopology` for the Loewner order on
-  matrices) together with a vector-valued `integral_mono`; neither is present in
-  Mathlib 4.31 (the matrix order supplies `IsOrderedAddMonoid` and
-  `StarOrderedRing`, but no `OrderClosedTopology` instance).  The
-  positive-semidefinite square root needed to package each `T(P i)` as a Kraus
-  term `C i * (C i)ᴴ` for `povm_resolvent_inv_le` is available as `CFC.sqrt`.
+* Monotonicity of the matrix-valued Bochner integral in the Loewner order is
+  now available: `TNLean.Channel.Basic` supplies the closed Loewner-order
+  topology on finite matrices, Mathlib supplies the ordered Bochner theorem
+  `integral_mono_ae`, and `TNLean.Channel.Schwarz.OperatorJensenAux` records
+  the positive-semidefinite integral specialization as
+  `integral_nonneg_matrix_of_ae`.  Pulling a positive linear map through the
+  integral can use `ContinuousLinearMap.integral_comp_comm` after packaging the
+  finite-dimensional map as a continuous linear map.  The remaining proof work
+  is the pointwise positive-map Jensen/resolvent step and its spectral
+  reduction to `povm_resolvent_inv_le`.  The positive-semidefinite square root
+  needed to package each `T(P i)` as a Kraus term `C i * (C i)ᴴ` is available as
+  `CFC.sqrt`.
 * Operator convexity of `rpow` over `[1, 2]`, the scalar input of
   `posMap_rpow_convex_jensen`, is now available as `CFC.convexOn_rpow` in
   `TNLean.Analysis.RpowConvexity`; the convex axiom therefore shares the single
@@ -99,9 +101,10 @@ The remaining Mathlib or local formalization gaps are:
    `povm_resolvent_inv_le` in `TNLean.Channel.Schwarz.OperatorJensenAux`, with
    the Kraus factorization `B i = (CFC.sqrt (B i)) * (CFC.sqrt (B i))ᴴ` and
    defect `(1 - ∑ i, B i)`.  What remains is integrating this pointwise bound:
-   the matrix-valued Bochner monotonicity step (`integral_mono` in the Loewner
-   order, needing the `OrderClosedTopology` instance flagged above) and the
-   commutation of `T` with the integral.
+   Mathlib's ordered Bochner monotonicity theorem, the local
+   positive-semidefinite integral specialization in
+   `TNLean.Channel.Schwarz.OperatorJensenAux`, and the commutation of `T` with
+   the integral.
 2. **Operator convexity of `rpow` for `p ∈ [1, 2]`**: use the
    decomposition `x^p = x · x^{p-1}` for `p ∈ [1, 2]` (Mathlib's
    `rpowIntegrand₁₂`), reducing to concavity of `x^{p-1}` for

TNLean/Channel/Schwarz/OperatorJensenAux.lean

@@ -3,9 +3,11 @@ Copyright (c) 2026 TNLean contributors. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: TNLean contributors
 -/
+import TNLean.Channel.Basic
 import Mathlib.Analysis.CStarAlgebra.Matrix
 import Mathlib.Analysis.Matrix.Order
 import Mathlib.LinearAlgebra.Matrix.PosDef
+import Mathlib.MeasureTheory.Integral.Bochner.Basic
 
 /-!
 # Finite-POVM compression lemmas for operator Jensen
@@ -36,6 +38,8 @@ representation; see the status note below.
   block-diagonal matrix yields the weighted sum of reciprocals.
 - `povm_resolvent_inv_le`: the finite-POVM resolvent inequality, the key
   algebraic step toward the concave real-power Jensen inequality.
+- `integral_nonneg_matrix_of_ae`: matrix-valued Bochner integrals preserve
+  almost-everywhere positive semidefiniteness.
 
 ## Status
 
@@ -54,8 +58,10 @@ integrand together with the resolvent form
 The remaining unfinished step is therefore the operator Jensen inequality for a
 positive subunital map `T` applied to a single integrand,
 `T(cfc (Real.rpowIntegrand₀₁ p t) A) ≤ cfc (Real.rpowIntegrand₀₁ p t) (T A)`,
-together with monotonicity of the matrix-valued integral in the Loewner order;
-combining these and integrating discharges `posMap_rpow_concave_jensen`.
+together with the spectral reduction to `povm_resolvent_inv_le`.  The
+matrix-valued positive-integral step is now packaged below from Mathlib's
+ordered Bochner integral API and the local closed Loewner-order topology on
+finite matrices; order monotonicity itself is Mathlib's `integral_mono_ae`.
 -/
 
 open scoped Matrix ComplexOrder MatrixOrder
@@ -113,6 +119,28 @@ end Matrix.PosDef
 
 namespace TNLean.OperatorJensen
 
+section MatrixBochnerOrder
+
+open MeasureTheory
+
+variable {α : Type*} [MeasurableSpace α] {μ : Measure α} {D : ℕ}
+
+/-- A matrix-valued Bochner integral is positive semidefinite when the integrand
+is positive semidefinite almost everywhere.  This is the Loewner-order
+specialization of Mathlib's ordered Bochner integral theorem, using the local
+closed-order instance for finite matrices from `TNLean.Channel.Basic`. -/
+lemma integral_nonneg_matrix_of_ae {f : α → Matrix (Fin D) (Fin D) ℂ}
+    (hpos : ∀ᵐ x ∂μ, (f x).PosSemidef) :
+    (∫ x, f x ∂μ).PosSemidef := by
+  have hnonneg : ∀ᵐ x ∂μ, (0 : Matrix (Fin D) (Fin D) ℂ) ≤ f x := by
+    filter_upwards [hpos] with x hx
+    simpa [Matrix.le_iff] using hx
+  have hint : (0 : Matrix (Fin D) (Fin D) ℂ) ≤ ∫ x, f x ∂μ :=
+    integral_nonneg_of_ae (μ := μ) (f := f) hnonneg
+  simpa [Matrix.le_iff] using hint
+
+end MatrixBochnerOrder
+
 section POVM
 
 variable {D : ℕ} {ι : Type*} [Fintype ι] [DecidableEq ι]

blueprint/src/chapter/ch18_operator_convexity.tex

@@ -228,10 +228,27 @@ \section{Operator Jensen inequality for positive maps}
     bound~(\ref{eq:opconv_povm_resolvent_bound}).
 \end{proof}
 
+\begin{lemma}[Positive matrix-valued integrals]\label{lem:operator_jensen_integral_order}
+    \lean{TNLean.OperatorJensen.integral_nonneg_matrix_of_ae}
+    \leanok
+    Let $f$ be a function from a measure space to a finite matrix algebra. If
+    $f(x)\ge0$ for almost every $x$, then
+    $\int f(x)\,d\mu(x)\ge0$.
+\end{lemma}
+
+\begin{proof}
+    \leanok
+    The Loewner order has closed positive cone in finite dimension. Hence the
+    ordered Bochner integral preserves almost-everywhere nonnegativity. The
+    corresponding almost-everywhere monotonicity statement is the general
+    ordered Bochner integral theorem.
+\end{proof}
+
 \begin{theorem}[Jensen for concave real powers]\label{thm:posMap_rpow_concave_jensen}
     \lean{posMap_rpow_concave_jensen}
     \notready
-    \uses{def:positive_map, lem:operator_jensen_povm_resolvent}
+    \uses{def:positive_map, lem:operator_jensen_povm_resolvent,
+        lem:operator_jensen_integral_order}
     For a positive subunital map $T$, a positive semidefinite matrix~$A$,
     and $p\in[0,1]$:
     \[

docs/audits/2026-04-22_issue138_op_convexity_blocker.md

@@ -14,6 +14,12 @@ Ando–Lieb goal.
 
 No honest proof edit to those declarations landed in this pass.
 
+Status update after the Mathlib 4.31 upgrade: the scalar functional-calculus
+inputs named below are now present in the formal development as
+`CFC.concaveOn_rpow`, `CFC.convexOn_rpow`, and `CFC.concaveOn_log`.  The remaining
+gap is the positive-map Jensen theorem for positive unital or subunital maps.
+The list below records the state of the April audit.
+
 ## Current available infrastructure
 
 ### Mathlib
@@ -30,14 +36,15 @@ Available on the current toolchain:
   $x \mapsto 1 - (1 + x)^{-1}$:
   `CFC.monotoneOn_one_sub_one_add_inv_real`
 
-Still explicitly missing upstream:
+At the time of the audit, the following items were still explicitly missing
+upstream:
 
 - operator concavity of $x^p$ on $[0,1]$
 - operator convexity of $x^p$ on $[1,2]$
 - operator concavity of $\log$
 - a general operator Jensen theorem for positive unital/subunital maps
 
-The current Mathlib source still says this out loud:
+At that time the Mathlib source still said this out loud:
 
 - `Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/Order.lean`
   lists TODOs for operator concavity/convexity of `rpow`
@@ -193,4 +200,4 @@ matrix-valued integral representation is currently available in Mathlib.
 A focused follow-up should target the smallest operator-valued Jensen API first,
 preferably in one of the equivalent forms above. Once that lands, the three
 Cor. 5.2 statements in `OperatorMonotone.lean` should collapse immediately, and
-only then does it become realistic to revisit the Ando–Lieb theorem.
+only then does it become realistic to revisit the Ando–Lieb theorem.

docs/paper-gaps/wolf_ch5_operator_jensen_lieb.tex

@@ -9,7 +9,7 @@
 
 \title{Wolf Chapter~5 Operator Jensen and Lieb Concavity Axioms}
 \author{}
-\date{2026-06-22}
+\date{2026-06-23}
 
 \begin{document}
 \maketitle
@@ -77,16 +77,10 @@ \subsection{The point at issue: the genuine gap is positive-map Jensen}
     together with the Bochner-integral convexity bridge for C\textsuperscript{*}-algebras.}
 and, through it, the operator concavity of $x\mapsto x^p$ on $[0,1]$
 (\leanid{CFC.concaveOn_rpow}) and of $\log$ (\leanid{CFC.concaveOn_log}).  The
-scalar inputs of the two concavity axioms are therefore already
-operator-concave in the formal library.  The scalar input of the convex axiom,
-operator convexity of $x\mapsto x^p$ on $[1,2]$, is \emph{not} yet in the
-library: only the operator-monotone and operator-concave $[0,1]$ lemmas exist,
-and operator convexity of \texttt{rpow} over $\mathrm{Icc}\,1\,2$ is an open
-upstream TODO.\footnote{%
-    \path{Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/Order.lean},
-    line~29.}
-That missing convexity lemma is, however, a small derivable increment
-(\S\ref{ssec:first-step}), not the deep obstruction.
+scalar input of the convex axiom, operator convexity of $x\mapsto x^p$ on
+$[1,2]$, is also now present as \leanid{CFC.convexOn_rpow} in
+\doclink{TNLean/Analysis/RpowConvexity}.  Thus the scalar functional-calculus
+inputs for the three Jensen axioms are available in the formal development.
 
 The remaining gap is the step \emph{from} operator concavity (a statement about a
 single operator) \emph{to} the Jensen inequality $T(fA)\le f(TA)$ for a positive
@@ -158,28 +152,20 @@ \subsection{The compression scaffold is faithful to bare
 integral representation of \texttt{rpow} to the operator inequality
 \leanid{posMap_rpow_concave_jensen}.
 
-\subsection{The concrete first step}\label{ssec:first-step}
-
-Independently of the positive-map Jensen step, one input is still missing from
-the formal library on the convex side: operator convexity of $x\mapsto x^p$ for
-$p\in[1,2]$.  Adding \leanid{CFC.convexOn_rpow} for $p\in[1,2]$ discharges the
-corresponding upstream TODO\footnote{%
-    \path{Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/Order.lean},
-    line~29.}
-and supplies the scalar operator-convexity input for
-\leanid{posMap_rpow_convex_jensen}.  It is obtained from the $[0,1]$ data
-already in the library through the Bendat--Sherman / Hansen--Pedersen
-characterization: for a continuous $f$ on $[0,\infty)$ with $f(0)\le 0$, $f$ is
-operator convex if and only if $x\mapsto f(x)/x$ is operator monotone.  Applied
-to $f(x)=x^p$ with $f(0)=0$, this gives the required statement on
-$[0,\infty)$: for each exponent $p\in[1,2]$, the function $x\mapsto x^p$ is
-operator convex once $x\mapsto x^{p-1}$ is operator monotone.  The latter is
-exactly \leanid{CFC.monotone_rpow} with exponent $p-1\in[0,1]$.  The bridge
-therefore runs through operator
-\emph{monotonicity}, not operator concavity: the naive identity
-$x^p = x\cdot x^{p-1}$ does \emph{not} establish operator convexity, since
-operator convexity is not preserved under multiplication by $x$.  This is the
-smallest reusable increment toward the convex power case.
+\subsection{Current formal inputs}\label{ssec:formal-inputs}
+
+The auxiliary ingredients needed before the final positive-map Jensen assembly
+are now present.  The theorem \leanid{CFC.convexOn_rpow} supplies operator
+convexity of $x\mapsto x^p$ for $p\in[1,2]$, completing the scalar
+functional-calculus input for \leanid{posMap_rpow_convex_jensen}.
+
+The closedness of the finite-dimensional Loewner cone also gives the ordered
+Bochner integral step needed for the integral route.  The positive-cone
+specialization is recorded as
+\leanid{TNLean.OperatorJensen.integral_nonneg_matrix_of_ae}: a matrix-valued
+Bochner integral of an almost-everywhere positive semidefinite function is
+positive semidefinite.  Almost-everywhere Loewner inequalities are integrated
+directly by the general ordered Bochner theorem \leanid{integral_mono_ae}.
 
 \subsection{Verdict}
 
@@ -190,8 +176,11 @@ \subsection{Verdict}
 representation of the integrand, previously named as the obstruction, is
 present.  The existing finite-POVM compression scaffold realises Wolf's
 positive-map route (\S\ref{ssec:caveat}) and is faithful to the bare positivity
-hypothesis; what remains is the Löwner-integral step that carries the pointwise
-resolvent inequality through the integral representation.
+hypothesis.  What remains is the spectral reduction of the pointwise
+positive-map resolvent inequality to
+\leanid{TNLean.OperatorJensen.povm_resolvent_inv_le}, followed by the final
+assembly through the ordered Bochner integral monotonicity theorem and the
+matrix-valued positive-integral specialization.
 
 \section{The Lieb concavity axiom}
 
@@ -286,10 +275,12 @@ \section*{References}
 F.~Hansen and G.~K.\ Pedersen, \emph{Jensen's operator inequality}, Bull.\
 London Math.\ Soc.\ \textbf{35} (2003) 553--564;
 R.~Bhatia, \emph{Matrix Analysis}, Springer GTM~169 (1997), Chapter~V.
-The relevant formal-library lemmas are
+The relevant formal-library inputs now available are
 \leanid{CFC.exists_measure_nnrpow_eq_integral_cfcₙ_rpowIntegrand₀₁},
-\leanid{CFC.concaveOn_rpow}, and \leanid{CFC.concaveOn_log}; the missing
-upstream item is \leanid{CFC.convexOn_rpow} for $p\in[1,2]$.
+\leanid{CFC.concaveOn_rpow}, \leanid{CFC.convexOn_rpow}, and
+\leanid{CFC.concaveOn_log}.  Thus the scalar functional-calculus inputs are
+available; the remaining unproved theorem is the positive-map Jensen step
+described above.
 
 \bibliographystyle{alpha}
 \bibliography{references}