feat(Channel/Schwarz): add positive-map rpow integrand Jensen

[LionSR]

Refs #778, #138, #3375.

Summary:

• Adds TNLean.OperatorJensen.positiveMap_rpowIntegrand₀₁_jensen for p ∈ (0,1) and t > 0.
• Proves the CFC resolvent form of Real.rpowIntegrand₀₁ and combines it with the existing positive-map resolvent inequality.
• Updates the operator-convexity axiom-status note and the Chapter 18 blueprint: the concave real-power Jensen axiom is now reduced to the Loewner-integral assembly step.

Scope:

• Does not remove posMap_rpow_concave_jensen yet.
• Does not touch the convex real-power or logarithmic Jensen axioms.

Validation:

• lake env lean TNLean/Channel/Schwarz/OperatorJensenAux.lean
• lake env lean TNLean/Axioms/OperatorConvexity.lean
• lake build TNLean passed, with only pre-existing warnings including the known periodic Case3 sorry warning.
• python3 scripts/blueprint_lean_sync.py --root . --ci
• leanblueprint checkdecls
• git diff --check
• rg -n "sorry|admit|native_decide|\\baxiom\\b" TNLean/Channel/Schwarz/OperatorJensenAux.lean found no matches.

---

Note

Low Risk
New proved lemmas and documentation only; no changes to axioms, APIs, or runtime behavior beyond the formalization layer.

Overview
Adds TNLean.OperatorJensen.positiveMap_rpowIntegrand₀₁_jensen, showing that for a positive subunital map T, PSD A, p ∈ (0,1), and t > 0, the Löwner-integral integrand satisfies T(cfc (Real.rpowIntegrand₀₁ p t) A) ≤ cfc (Real.rpowIntegrand₀₁ p t) (T A).

The proof introduces a private CFC resolvent rewrite for Real.rpowIntegrand₀₁ and combines it with the existing positiveMap_resolvent_inv_le estimate. OperatorJensenAux gains an import from Mathlib’s rpow integral representation module.

OperatorConvexity status notes and the Chapter 18 blueprint are updated: the concave real-power Jensen route now treats the per-integrand step as proved and leaves Löwner-integral assembly as the remaining work toward posMap_rpow_concave_jensen (still an axiom). The blueprint adds lemma lem:operator_jensen_positive_map_rpow_integrand and wires it into the not-yet-ready concave Jensen theorem.

^{Reviewed by Cursor Bugbot for commit 2a3fa67. Bugbot is set up for automated code reviews on this repo. Configure here.}

[chatgpt-codex-connector]

You have reached your Codex usage limits for code reviews. You can see your limits in the Codex usage dashboard.

[claude]

Review Summary

Verdict: 🟡 REQUEST CHANGES — one 🟡 issue must be addressed before approval.

---

What this PR does (correct assessment)

The PR adds positiveMap_rpowIntegrand₀₁_jensen, proving the per-integrand Jensen inequality T(cfc(Real.rpowIntegrand₀₁ p t) A) ≤ cfc(Real.rpowIntegrand₀₁ p t) (T A) for a positive subunital map T, p ∈ (0,1), and t > 0. The proof strategy — CFC resolvent rewrite followed by scaling the existing positiveMap_resolvent_inv_le — is mathematically correct. The hypothesis set matches the cited source (Wolf Corollary 5.2 / Hansen–Pedersen route). The blueprint additions are accurate: the new lemma lem:operator_jensen_positive_map_rpow_integrand is correctly tagged with \leanok and \lean{...}, and its \uses dependency on the resolvent lemma is correct.

Checklist by category

Category	Status
🔴 Proof integrity	✅ No sorry, admit, axiom, native_decide, or kernel bypasses
🔴 Proof correctness	✅ Mathematical reasoning is sound; CFC-to-resolvent rewrite and algebraic scaling are correct
🟡 Mathlib style	❌ 1 issue — see inline comment on line 758
🔴 Type safety	✅ No universe, instance, or coercion issues
🟡 Performance	✅ No timeout risks beyond the style issue flagged
🟡 Modularity & duplication	ℹ️ 1 advisory — see inline comment on line 698
🟡 Documentation	✅ New lemma has a clear docstring; blueprint proof sketch is accurate
🟡 Paper-gap notes	✅ No paper-gap notes changed

Blocking issue

🟡 Lines 758–762 — Unstructured simp/ring_nf block with commutativity lemmas. The ext i j; simp [..., add_comm, add_left_comm, add_assoc]; simp; ring_nf block drops to entry-wise algebra with dangerous simp commutativity lemmas, breaking the structured matrix-algebra style used throughout the rest of the file. See the inline comment for a concrete suggested fix using a matrix-level identity lemma. This must be restructured before approval.

Non-blocking advisory

ℹ️ Line 698 — cfc_rpowIntegrand₀₁_eq_resolvent duplicates Mathlib's concaveOn_cfc_rpowIntegrand₀₁ EqOn block. Mathlib does not yet export this as a standalone lemma, so the private helper is fine for now. A comment noting the duplication would be helpful, and an upstream extraction to Mathlib is desirable long-term. See the inline comment.

Blueprint

• New lemma lem:operator_jensen_positive_map_rpow_integrand — correct \lean/\leanok tags and accurate proof sketch.
• Updated \uses of thm:posMap_rpow_concave_jensen — correct transitive dependency (integrand lemma → resolvent lemma).
• Status note updates in OperatorConvexity.lean — accurate reflection of the remaining Löwner-integral assembly gap.

[claude]

🟡 Mathlib style / Performance: The proof of positiveMap_rpowIntegrand₀₁_jensen closes with an unstructured entry-wise algebra block:

  convert hscaled using 1
  ext i j
  simp [LinearMap.map_smul_of_tower, sub_eq_add_neg, smul_add, add_comm,
    add_left_comm, add_assoc]
  simp [ht_powC₂]
  ring_nf

Two concerns:

1. simp with commutativity lemmas is dangerous. Including add_comm, add_left_comm, add_assoc in simp can cause non-termination or produce unexpected normal forms. Use abel or ring for additive identities, or restructure.

2. Entry-wise ext i j defeats structured matrix algebra. The surrounding lemmas in this file (e.g., povm_resolvent_inv_le, positiveMap_resolvent_inv_le) work at the matrix level with calc blocks, rw, and simpa. The switch to entry-wise simp/ring_nf is inconsistent with this style and makes the proof brittle — if the matrix expressions change shape, the entry-wise normal form will break silently.

Suggested fix: Prove a matrix-level identity lemma:

  have hmatrix_diff : cfc (Real.rpowIntegrand₀₁ p t) (T A) - T (cfc (Real.rpowIntegrand₀₁ p t) A) =
      t ^ p • (T ((A + t • (1 : MatD))⁻¹) + t⁻¹ • (1 - T 1) - ((T A) + t • (1 : MatD))⁻¹) := by
    rw [hAeq, hTAeq]
    calc
      _ = ... := by
        simp [map_sub, map_smul, sub_sub, smul_sub, sub_smul]
      ...
  simpa [hmatrix_diff, Matrix.le_iff] using hscaled

This keeps the proof at the matrix level, eliminates the entry-wise expansion, and avoids simp with commutativity lemmas.

This must be fixed before approval.

[claude]

ℹ️ Advisory — Mathlib duplication: The private lemma cfc_rpowIntegrand₀₁_eq_resolvent replicates the EqOn computation from Mathlib's CFC.concaveOn_cfc_rpowIntegrand₀₁ (in Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/IntegralRepresentation.lean, lines 580–582). Mathlib does not currently export a standalone resolvent-form lemma, so this private helper is a reasonable internal convenience. However, the duplication should be noted in a comment, and ideally an upstream PR to Mathlib should extract cfc_rpowIntegrand₀₁_eq_resolvent as a public lemma — then this project file can drop its private copy and import the Mathlib version.

Suggested: add a brief comment above cfc_rpowIntegrand₀₁_eq_resolvent noting the duplication:

/-- Resolvent form of the Löwner-integral integrand
`Real.rpowIntegrand₀₁ p t` under the continuous functional calculus.

**Note:** This `EqOn` computation is identical to the one inside
Mathlib's `CFC.concaveOn_cfc_rpowIntegrand₀₁`; it is private here
because Mathlib does not (yet) export it as a standalone lemma. -/