Operator convexity / concavity for matrix functions (foundational rungs)

This file develops the first rungs of the operator-convexity ladder over Hermitian / positive-definite complex matrices, using the Löwner order (Matrix.instPartialOrder, scoped MatrixOrder: A ≤ B := (B - A).PosSemidef) and the continuous functional calculus cfc.

Main definitions

• Matrix.OperatorConvexOn s f / Matrix.OperatorConcaveOn s f : a real function f is operator convex (resp. concave) on s ⊆ ℝ if, for every finite index type n and all Hermitian A, B : Matrix n n ℂ whose spectra (and the spectrum of their convex combination) lie in s, the CFC satisfies cfc f (t • A + (1 - t) • B) ≤ t • cfc f A + (1 - t) • cfc f B (resp. ≥) for t ∈ [0,1]. Operator convexity is genuinely an all-dimensions notion, so the predicate quantifies over n.

Main results

• Matrix.inv_loewner_convex : the Löwner inverse inequality for positive-definite matrices, (t A + (1-t) B)⁻¹ ≤ t A⁻¹ + (1-t) B⁻¹, proved via the Schur-complement PSD characterisation Matrix.PosDef.fromBlocks₁₁.
• Matrix.cfc_inv_posDef : cfc (·⁻¹) A = A⁻¹ for positive-definite A (CFC ↔ matrix inverse bridge).
• Matrix.operatorConvexOn_inv : x ↦ x⁻¹ is operator convex on (0, ∞) (the predicate form, the foundational rung L.1 of the ladder).
• Matrix.inv_shift_loewner_convex / Matrix.operatorConcaveOn_neg_add_inv : the shifted resolvent x ↦ (x + s)⁻¹ is operator convex, equivalently x ↦ -(x + s)⁻¹ is operator concave, for each s > 0 (the L.2 per-shift building block; the negation of L.1 translated by s).
• Matrix.OperatorConcaveOn.affine_output : the increasing-affine output transform f ↦ (fun x => c * f x + d) with c ≥ 0 preserves operator concavity (the Step-C algebra in the log route, c = p⁻¹, d = -p⁻¹, lifting x^p concavity to p⁻¹(x^p − 1) concavity).
• Matrix.operatorConcaveOn_iff_concaveOn (and the two one-directional lemmas operatorConcaveOn_of_concaveOn, concaveOn_of_operatorConcaveOn) : the reframing lemma — OperatorConcaveOn s f is equivalent to ordinary ConcaveOn ℝ (spectralSet s n) (fun A => cfc f A) for every dimension n, where spectralSet s n is the set of Hermitian matrices with spectrum ⊆ s and the codomain carries the Löwner order. This makes Mathlib's whole ConcaveOn API (ConcaveOn.add, .smul, .add_const, Jensen, …) applicable to operator concavity. The reframing is faithful: the ConcaveOn inequality a • cfc f A + b • cfc f B ≤ cfc f (a • A + b • B) (a + b = 1, a, b ≥ 0, Löwner ≤) is exactly the operator-concavity inequality, not a scalar/trace weakening.
• Matrix.convex_spectralSet_Ioi : spectralSet (Set.Ioi 0) n is Convex ℝ (a convex combination of positive-definite Hermitian matrices is positive definite), the domain-convexity side condition of the (0, ∞) reframing.
• Matrix.operatorConcaveOn_rpow_zero / operatorConcaveOn_rpow_one : x ↦ x ^ (0 : ℝ) and x ↦ x ^ (1 : ℝ) (Real.rpow) are operator concave on (0, ∞) — the trivial endpoints of the L.3a target. The interior p ∈ (0, 1) is not proved here (see the implementation note and specs/operator-convexity-plan.md for the precise integral-assembly wall).

Implementation notes

The convex combination is taken with complex scalars (t : ℂ) rather than real scalars: the Matrix.PosSemidef.smul API requires 0 ≤ (a : ℂ) (a ComplexOrder nonnegativity), and Complex.coe_smul bridges (t : ℂ) • A = (t : ℝ) • A. This is the natural setting for matrices over ℂ and does not weaken the statement.

Category: 1-Mathlib (CSD-free; staged as a Mathlib upstream candidate). Natural Mathlib namespace Matrix.

Provenance

Foundational rungs (L.0 predicate + L.1 inverse) of the operator-convexity ladder whose summit is the data-processing inequality hDPI of CsdLean4.Mathlib.QuantumInfo.StrongSubadditivity.strong_subadditivity_of_relEntropy_monotone (K1-C). The ladder L.1 → L.5 is recorded in specs/operator-convexity-plan.md.

Tags

operator convex, operator monotone, Löwner order, Schur complement, functional calculus

The operator-convexity predicate (L.0)

def Matrix.OperatorConvexOn (s : Set ℝ) (f : ℝ → ℝ) : Prop

OperatorConvexOn s f : the real function f is operator convex on s ⊆ ℝ.

For every finite index type n and all Hermitian A B : Matrix n n ℂ with spectra (and the spectrum of t A + (1-t) B) contained in s, and every t ∈ [0,1], the continuous functional calculus satisfies the Löwner inequality cfc f (t • A + (1 - t) • B) ≤ t • cfc f A + (1 - t) • cfc f B.

The quantification is over all dimensions n: operator convexity is strictly stronger than ordinary (scalar) convexity and is a genuinely dimension-uniform notion.

Equations

• One or more equations did not get rendered due to their size.

def Matrix.OperatorConcaveOn (s : Set ℝ) (f : ℝ → ℝ) : Prop

OperatorConcaveOn s f : the real function f is operator concave on s ⊆ ℝ, i.e. -f is operator convex. Equivalently, the reversed Löwner inequality holds.

Equations

• One or more equations did not get rendered due to their size.

L.1 : operator convexity of x ↦ x⁻¹

theorem Matrix.fromBlocks_inv_posSemidef {n : Type u_1} [Fintype n] [DecidableEq n] {A : Matrix n n ℂ} (hA : A.PosDef) : (fromBlocks A 1 1 A⁻¹).PosSemidef

For a positive-definite A, the block matrix ⟦A, 1; 1, A⁻¹⟧ is positive semidefinite. This is the Schur-complement witness of operator convexity of the inverse: the Schur complement of the A-block is A⁻¹ - 1·A⁻¹·1 = 0 ≥ 0.

theorem Matrix.convexComb_posDef {n : Type u_1} {A B : Matrix n n ℂ} (hA : A.PosDef) (hB : B.PosDef) {t : ℝ} (ht0 : 0 ≤ t) (ht1 : t ≤ 1) : (↑t • A + (1 - ↑t) • B).PosDef

A convex combination (complex weights t, 1-t ∈ [0,1]) of positive-definite matrices is positive definite.

theorem Matrix.inv_loewner_convex {n : Type u_1} [Fintype n] [DecidableEq n] {A B : Matrix n n ℂ} (hA : A.PosDef) (hB : B.PosDef) {t : ℝ} (ht0 : 0 ≤ t) (ht1 : t ≤ 1) : (↑t • A + (1 - ↑t) • B)⁻¹ ≤ ↑t • A⁻¹ + (1 - ↑t) • B⁻¹

Operator convexity of the matrix inverse (Löwner form). For positive-definite A, B and t ∈ [0,1], (t • A + (1 - t) • B)⁻¹ ≤ t • A⁻¹ + (1 - t) • B⁻¹ in the Löwner order. Proof: convexity of the PSD cone applied to the Schur-complement block witnesses ⟦A,1;1,A⁻¹⟧, then the backward Schur characterisation Matrix.PosDef.fromBlocks₁₁.

CFC ↔ matrix-inverse bridge

theorem Matrix.posDef_spectrum_pos {n : Type u_1} [Fintype n] [DecidableEq n] {A : Matrix n n ℂ} (hA : A.PosDef) (x : ℝ) : x ∈ spectrum ℝ A → 0 < x

The real spectrum of a positive-definite matrix is positive.

theorem Matrix.cfc_inv_posDef {n : Type u_1} [Fintype n] [DecidableEq n] {A : Matrix n n ℂ} (hA : A.PosDef) : cfc (fun (x : ℝ) => x⁻¹) A = A⁻¹

For positive-definite A, the continuous functional calculus of x ↦ x⁻¹ agrees with the matrix (nonsingular) inverse: cfc (·⁻¹) A = A⁻¹.

theorem Matrix.posDef_of_spectrum_pos {n : Type u_1} [Fintype n] [DecidableEq n] {A : Matrix n n ℂ} (hA : A.IsHermitian) (hspec : ∀ x ∈ spectrum ℝ A, 0 < x) : A.PosDef

A Hermitian matrix whose real spectrum is positive is positive definite.

L.1, predicate form

theorem Matrix.operatorConvexOn_inv : OperatorConvexOn (Set.Ioi 0) fun (x : ℝ) => x⁻¹

L.1 of the ladder. The function x ↦ x⁻¹ is operator convex on (0, ∞).

This is the predicate-form repackaging of inv_loewner_convex via the CFC ↔ matrix-inverse bridge cfc_inv_posDef: a Hermitian matrix with spectrum in (0, ∞) is positive definite.

Shifted-inverse rungs (the resolvent family x ↦ (x + s)⁻¹)

These are the building blocks of the integral-representation route to operator concavity of log and x ↦ x^p: each resolvent x ↦ -(x + s)⁻¹ is operator concave (a translate + negate of L.1's inv_loewner_convex), and the target functions are positive integral mixtures of these. They are proved here directly in the matrix / Löwner / CFC setting, with no new axiom.

theorem Matrix.add_smul_one_posDef {n : Type u_1} [DecidableEq n] {A : Matrix n n ℂ} (hA : A.PosDef) {s : ℝ} (hs : 0 < s) : (A + ↑s • 1).PosDef

For positive-definite A and s > 0, the shifted matrix A + s • 1 is positive definite.

theorem Matrix.posDef_add_pos {n : Type u_1} [Fintype n] [DecidableEq n] {A : Matrix n n ℂ} (hA : A.PosDef) {s : ℝ} (hs : 0 ≤ s) (x : ℝ) : x ∈ spectrum ℝ A → 0 < x + s

The real spectrum of a positive-definite matrix shifted by s ≥ 0 is bounded below by s, hence x + s ≠ 0 whenever x is in the spectrum and s > 0 (or x > 0).

theorem Matrix.cfc_add_inv_posDef {n : Type u_1} [Fintype n] [DecidableEq n] {A : Matrix n n ℂ} (hA : A.PosDef) {s : ℝ} (hs : 0 < s) : cfc (fun (x : ℝ) => (x + s)⁻¹) A = (A + ↑s • 1)⁻¹

CFC ↔ shifted matrix inverse bridge. For positive-definite A and s > 0, the continuous functional calculus of x ↦ (x + s)⁻¹ agrees with the matrix inverse of the shift: cfc (fun x => (x + s)⁻¹) A = (A + s • 1)⁻¹.

theorem Matrix.inv_shift_loewner_convex {n : Type u_1} [Fintype n] [DecidableEq n] {A B : Matrix n n ℂ} (hA : A.PosDef) (hB : B.PosDef) {t : ℝ} (ht0 : 0 ≤ t) (ht1 : t ≤ 1) {s : ℝ} (hs : 0 < s) : (↑t • A + (1 - ↑t) • B + ↑s • 1)⁻¹ ≤ ↑t • (A + ↑s • 1)⁻¹ + (1 - ↑t) • (B + ↑s • 1)⁻¹

Operator convexity of the resolvent x ↦ (x + s)⁻¹ (Löwner form). For positive-definite A, B, t ∈ [0,1] and s > 0, (t • A + (1 - t) • B + s • 1)⁻¹ ≤ t • (A + s • 1)⁻¹ + (1 - t) • (B + s • 1)⁻¹. This is inv_loewner_convex applied to the PD shifts A + s • 1, B + s • 1, using that the convex combination of the shifts is the shift of the convex combination (since t + (1-t) = 1).

Predicate-form resolvent concavity

theorem Matrix.cfc_neg_add_inv_posDef {n : Type u_1} [Fintype n] [DecidableEq n] {A : Matrix n n ℂ} (hA : A.PosDef) {s : ℝ} (hs : 0 < s) : cfc (fun (x : ℝ) => -(x + s)⁻¹) A = -(A + ↑s • 1)⁻¹

The CFC of the negated resolvent x ↦ -(x + s)⁻¹ on a positive-definite matrix is -(A + s • 1)⁻¹.

theorem Matrix.operatorConcaveOn_neg_add_inv {s : ℝ} (hs : 0 < s) : OperatorConcaveOn (Set.Ioi 0) fun (x : ℝ) => -(x + s)⁻¹

Operator concavity of the negated resolvent. For each s > 0, the function x ↦ -(x + s)⁻¹ is operator concave on (0, ∞). This is the per-shift building block of the integral-representation route to operator concavity of log and x ↦ x^p: each negated resolvent is operator concave, and those target functions are positive integral mixtures of these resolvents. Proof: the negation of inv_shift_loewner_convex.

Affine output transform preserves operator concavity

The map f ↦ (fun x => c * f x + d) with c ≥ 0 is the increasing-affine transform of the output; it preserves operator concavity. This is the algebraic step needed to pass from x ↦ x ^ p operator concave to x ↦ p⁻¹ (x ^ p − 1) operator concave (Step C of the log route: c = p⁻¹ > 0, d = -p⁻¹).

theorem Matrix.cfc_affine_output {n : Type u_1} [Fintype n] [DecidableEq n] {A : Matrix n n ℂ} (hA : A.IsHermitian) {c d : ℝ} {f : ℝ → ℝ} (hf : ContinuousOn f (spectrum ℝ A)) : cfc (fun (x : ℝ) => c * f x + d) A = ↑c • cfc f A + ↑d • 1

CFC of an increasing-affine output transform: for Hermitian A and f continuous on the spectrum, cfc (fun x => c * f x + d) A = c • cfc f A + d • 1.

theorem Matrix.OperatorConcaveOn.affine_output {s : Set ℝ} {f : ℝ → ℝ} (hf : OperatorConcaveOn s f) {c d : ℝ} (hc : 0 ≤ c) (hcont : ∀ {m : Type} [inst : Fintype m] [inst_1 : DecidableEq m] {M : Matrix m m ℂ}, M.IsHermitian → ContinuousOn f (spectrum ℝ M)) : OperatorConcaveOn s fun (x : ℝ) => c * f x + d

Affine output transform preserves operator concavity. If f is operator concave on s and c ≥ 0, then x ↦ c * f x + d is operator concave on s, provided f is continuous on each relevant spectrum (hcont), which is needed for the CFC of the transform to split. This is the algebraic step in the log route: with c = p⁻¹ ≥ 0, d = -p⁻¹, it lifts operator concavity of x ↦ x^p to operator concavity of x ↦ p⁻¹ (x^p − 1).

The reframing lemma : operator concavity ↔ ordinary ConcaveOn of A ↦ cfc f A

This is the high-leverage unlock of the ladder. OperatorConcaveOn s f (the all-dimensions Löwner predicate) is equivalent to ordinary ConcaveOn ℝ (spectralSet s n) (fun A => cfc f A) for every finite dimension n, where the codomain Matrix n n ℂ carries the Löwner order (Matrix.instPartialOrder). The reframing is faithful, not a weakening: the ConcaveOn inequality a • cfc f A + b • cfc f B ≤ cfc f (a • A + b • B) (with a + b = 1, a, b ≥ 0 and ≤ the Löwner/PSD-cone order) is literally the operator-concavity inequality with a = t, b = 1 - t (the convex combination matches via Complex.coe_smul : (t : ℂ) • A = (t : ℝ) • A). Through it, Mathlib's whole ConcaveOn API — ConcaveOn.add, ConcaveOn.smul, ConcaveOn.add_const, the Jensen inequalities — applies to operator concavity for free.

def Matrix.spectralSet (s : Set ℝ) (n : Type u_2) [Fintype n] [DecidableEq n] : Set (Matrix n n ℂ)

The convex domain set of the reframing: the Hermitian matrices of dimension n whose spectrum lies in s ⊆ ℝ. For convex s this set is Convex ℝ (the domain-convexity side condition of ConcaveOn); see convex_spectralSet_Ioi for the (0, ∞) instance used by the ladder.

Equations

• Matrix.spectralSet s n = {A : Matrix n n ℂ | A.IsHermitian ∧ spectrum ℝ A ⊆ s}

@[simp]

theorem Matrix.mem_spectralSet {n : Type u_1} [Fintype n] [DecidableEq n] {s : Set ℝ} {A : Matrix n n ℂ} : A ∈ spectralSet s n ↔ A.IsHermitian ∧ spectrum ℝ A ⊆ s

theorem Matrix.convex_spectralSet_Ioi {n : Type u_1} [Fintype n] [DecidableEq n] : Convex ℝ (spectralSet (Set.Ioi 0) n)

spectralSet (Set.Ioi 0) n is Convex ℝ: a convex combination of positive-definite Hermitian matrices is positive definite (convexComb_posDef), and positive definiteness is exactly spectrum ℝ ⊆ (0, ∞) for Hermitian matrices. This is the domain-convexity side condition of the (0, ∞) reframing, hence of the whole x^p / log operator-concavity programme.

theorem Matrix.operatorConcaveOn_of_concaveOn {s : Set ℝ} {f : ℝ → ℝ} (h : ∀ (m : Type) [inst : Fintype m] [inst_1 : DecidableEq m], ConcaveOn ℝ (spectralSet s m) fun (A : Matrix m m ℂ) => cfc f A) : OperatorConcaveOn s f

Reframing, backward direction (the L.3a unlock). If, for every dimension m, the map A ↦ cfc f A is ordinary-ConcaveOn ℝ (spectralSet s m) (Löwner codomain), then f is OperatorConcaveOn s. This is the direction that lets the operator-concavity programme consume Mathlib's ConcaveOn API: prove ConcaveOn ℝ (spectralSet s m) (cfc f ·) by whatever convex-analysis route, and conclude operator concavity. No domain-convexity hypothesis is needed (it is bundled inside each ConcaveOn).

theorem Matrix.concaveOn_of_operatorConcaveOn {s : Set ℝ} {f : ℝ → ℝ} {n : Type} [Fintype n] [DecidableEq n] (hf : OperatorConcaveOn s f) (hconv : Convex ℝ (spectralSet s n)) : ConcaveOn ℝ (spectralSet s n) fun (A : Matrix n n ℂ) => cfc f A

Reframing, forward direction. If f is OperatorConcaveOn s and the domain spectralSet s n is Convex ℝ (e.g. convex_spectralSet_Ioi for s = (0, ∞)), then A ↦ cfc f A is ordinary-ConcaveOn ℝ (spectralSet s n) in the Löwner-ordered codomain. The Convex hypothesis is genuinely required (it is the first conjunct of ConcaveOn and is a fact about s, not derivable from operator concavity).

theorem Matrix.operatorConcaveOn_iff_concaveOn {s : Set ℝ} {f : ℝ → ℝ} (hconv : ∀ (m : Type) [inst : Fintype m] [inst_1 : DecidableEq m], Convex ℝ (spectralSet s m)) : OperatorConcaveOn s f ↔ ∀ (m : Type) [inst : Fintype m] [inst_1 : DecidableEq m], ConcaveOn ℝ (spectralSet s m) fun (A : Matrix m m ℂ) => cfc f A

The reframing lemma (full equivalence). Given that spectralSet s m is Convex ℝ in every dimension m (the domain-convexity side condition; supplied by convex_spectralSet_Ioi for s = (0, ∞)), operator concavity of f on s is equivalent to ordinary concavity of A ↦ cfc f A on spectralSet s m for every m, in the Löwner-ordered matrix codomain.

L.3a endpoints : x ↦ x ^ p operator concave on (0, ∞) at p ∈ {0, 1}

The interior p ∈ (0, 1) of the L.3a target (x ↦ x ^ p operator concave, Real.rpow) is not proved here: it requires the operator integral representation cfc (· ^ p) A = ∫ cfc (integrand t) A ∂μ (each integrand x ↦ x / (x + t) is operator concave via operatorConcaveOn_neg_add_inv + OperatorConcaveOn.affine_output), and the "cfc commutes with the integral" engine (cfcₙ_setIntegral) fires only for [NonUnitalCStarAlgebra A], which Matrix n n ℂ is not at the default instances (the C⋆-matrix structure lives on the CStarMatrix type synonym, and the rpow transport across it is blocked by the NonnegSpectrumClass/Pow instance-resolution wall recorded in OperatorConvexBridge.lean). See specs/operator-convexity-plan.md, L.3a, for the precise gap. The two endpoints below are immediate (constant 1 and the identity) and exercise the reframing machinery on the genuine Real.rpow.

theorem Matrix.operatorConcaveOn_rpow_zero : OperatorConcaveOn (Set.Ioi 0) fun (x : ℝ) => x ^ 0

L.3a endpoint p = 0. x ↦ x ^ (0 : ℝ) (Real.rpow) is operator concave on (0, ∞): on a positive-definite argument cfc (· ^ (0:ℝ)) A = cfc (fun _ => 1) A = 1, so both sides of the concavity inequality collapse to 1 (and 1 ≤ 1 in the Löwner order).

theorem Matrix.operatorConcaveOn_rpow_one : OperatorConcaveOn (Set.Ioi 0) fun (x : ℝ) => x ^ 1

L.3a endpoint p = 1. x ↦ x ^ (1 : ℝ) (Real.rpow) is operator concave on (0, ∞): it is the identity (cfc (· ^ (1:ℝ)) A = cfc id A = A), and the identity is operator affine, so the concavity inequality holds with equality (a • A + b • B = a • A + b • B).

A1 : the cfc-integral commutation lemma, and the Löwner-order topology instances

To assemble the interior p ∈ (0,1) of L.3a we must integrate matrix-valued functions over the resolvent parameter. The Bochner integral over Matrix n n ℂ requires a norm; we activate the Frobenius norm (open scoped Matrix.Norms.Frobenius), which is PiLp 2, hence finite dimensional and complete. The Frobenius topology is the standard product topology, so it is compatible with the Löwner order; in particular the PSD cone is closed (isClosed_posSemidef), giving the ClosedIciTopology / OrderClosedTopology / IsOrderedModule instances that the generic Bochner monotonicity / integral-of-concave lemmas (MeasureTheory.integral_concaveOn_of_integrand_ae) consume.

The Frobenius instances are scoped: they do not leak to importers of this module.

instance Matrix.instFiniteDimensionalRealComplex_csdLean4 {n : Type} [Fintype n] : FiniteDimensional ℝ (Matrix n n ℂ)

Matrix n n ℂ is finite dimensional over ℝ (via FiniteDimensional ℂ → ℝ); needed for the continuity of the entry-projection linear maps and for the completeness of the matrix space, which the Bochner integral requires.

@[instance_reducible]

noncomputable def Matrix.instNormedAddCommGroupMatrix {n : Type} [Fintype n] : NormedAddCommGroup (Matrix n n ℂ)

The (entrywise-sup) NormedAddCommGroup on Matrix n n ℂ, re-topologised so its bundled TopologicalSpace is syntactically the ambient product topology. This is the single normed structure the Bochner-integral lemmas use; it gives Integrable/∫/ContinuousENorm a consistent topology without disturbing cfc.

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

noncomputable def Matrix.instNormedSpaceRealMatrix {n : Type} [Fintype n] : NormedSpace ℝ (Matrix n n ℂ)

NormedSpace ℝ for the re-topologised norm (same norm as the elementwise one, so the norm_smul_le proof carries over verbatim).

Equations

• Matrix.instNormedSpaceRealMatrix = { toModule := Matrix.module, norm_smul_le := ⋯ }

@[instance_reducible]

noncomputable def Matrix.instNormedSpaceComplexMatrix {n : Type} [Fintype n] : NormedSpace ℂ (Matrix n n ℂ)

NormedSpace ℂ for the re-topologised norm; needed to rebuild a matrix from its entries (Integrable.smul_const) in matrix_integrable_of_entry.

Equations

• Matrix.instNormedSpaceComplexMatrix = { toModule := Matrix.module, norm_smul_le := ⋯ }

theorem Matrix.matrix_integral_apply {n : Type} [Fintype n] {μ : MeasureTheory.Measure ℝ} {F : ℝ → Matrix n n ℂ} (hF : MeasureTheory.Integrable F μ) (i j : n) : (∫ (s : ℝ), F s ∂μ) i j = ∫ (s : ℝ), F s i j ∂μ

Entrywise integral commutation. The Bochner integral of a matrix-valued integrable family is computed entrywise. Proof: each entry projection entryLinearMap ℝ ℂ i j is a (finite-dimensional, hence continuous) ℝ-linear map; ContinuousLinearMap.integral_comp_comm pulls it through.

theorem Matrix.matrix_integrable_of_entry {n : Type} [Fintype n] [DecidableEq n] {μ : MeasureTheory.Measure ℝ} {F : ℝ → Matrix n n ℂ} (hent : ∀ (i j : n), MeasureTheory.Integrable (fun (s : ℝ) => F s i j) μ) : MeasureTheory.Integrable F μ

Matrix integrability from entrywise integrability. If every entry s ↦ F s i j is integrable then so is the matrix family F, via the finite basis decomposition F s = ∑ i j, F s i j • single i j 1.

theorem Matrix.cfc_eq_eigenvectorUnitary_mul {n : Type} [Fintype n] [DecidableEq n] {A : Matrix n n ℂ} (hA : A.IsHermitian) (f : ℝ → ℝ) : cfc f A = (↑hA.eigenvectorUnitary * diagonal fun (k : n) => ↑(f (hA.eigenvalues k))) * star ↑hA.eigenvectorUnitary

The spectral (conjugation) form of the Hermitian CFC as a bare matrix product: cfc f A = U · diagonal (ofReal ∘ f ∘ λ) · Uᴴ, where U = hA.eigenvectorUnitary, λ = hA.eigenvalues. This is Matrix.IsHermitian.cfc_eq unfolded through Unitary.conjStarAlgAut_apply.

theorem Matrix.conj_diagonal_apply {n : Type} [Fintype n] [DecidableEq n] (U : Matrix n n ℂ) (v : n → ℂ) (i j : n) : (U * diagonal v * star U) i j = ∑ k : n, U i k * v k * star U k j

Entry of the spectral conjugation (U · diagonal v · star U) i j = ∑ k, U i k · v k · (star U) k j.

theorem Matrix.cfc_integral_commute {n : Type} [Fintype n] [DecidableEq n] {μ : MeasureTheory.Measure ℝ} {A : Matrix n n ℂ} (hA : A.IsHermitian) {g : ℝ → ℝ → ℝ} (hg : ∀ (k : n), MeasureTheory.Integrable (fun (s : ℝ) => g s (hA.eigenvalues k)) μ) (hcfc : MeasureTheory.Integrable (fun (s : ℝ) => cfc (g s) A) μ) : ∫ (s : ℝ), cfc (g s) A ∂μ = cfc (fun (x : ℝ) => ∫ (s : ℝ), g s x ∂μ) A

A1 — the cfc-integral commutation lemma. For a Hermitian A, a parameter family g : ℝ → ℝ → ℝ, a measure μ, with

• hg : each spectral-evaluation s ↦ g s (λ k) integrable, k over the eigenvalues, and
• hcfc: the matrix family s ↦ cfc (g s) A Bochner-integrable,

integration commutes with the continuous functional calculus: ∫ s, cfc (g s) A ∂μ = cfc (fun x => ∫ s, g s x ∂μ) A.

Route (spectral, entrywise): both sides equal U · diagonal (·) · Uᴴ; the eigenvector unitary U and Uᴴ are constant, so the equality reduces to the finite family of scalar identities ∫ s, g s (λ k) ∂μ = (∫ s, g s · ∂μ)(λ k), pulled through the integral by linearity of the entry projection and integral_ofReal. No C⋆-Bochner machinery is needed — this is the matrix-carrier unlock that the CStarMatrix route could not reach (NonUnitalCStarAlgebra (Matrix n n ℂ) fails).

Löwner-order topology instances on the ambient (product) matrix topology

theorem Matrix.isClosed_posSemidef {n : Type} [Fintype n] : IsClosed {M : Matrix n n ℂ | M.PosSemidef}

The PSD cone is closed in the Frobenius topology. It is the intersection of the closed Hermitian subspace {M | Mᴴ = M} with the closed half-spaces {M | 0 ≤ star x ⬝ᵥ (M *ᵥ x)} (x ranging over n → ℂ), each closed since M ↦ star x ⬝ᵥ (M *ᵥ x) is continuous and {z : ℂ | 0 ≤ z} is closed.

instance Matrix.instClosedIciTopologyComplex_csdLean4 {n : Type} [Fintype n] : ClosedIciTopology (Matrix n n ℂ)

The Löwner [a, +∞) is closed: Ici a = (· - a) ⁻¹' (PSD cone).

instance Matrix.instOrderClosedTopologyComplex_csdLean4 {n : Type} [Fintype n] : OrderClosedTopology (Matrix n n ℂ)

The Löwner order relation is closed: {(x,y) | x ≤ y} = (fun p => p.2 - p.1) ⁻¹' (PSD cone).

instance Matrix.instPosSMulMonoRealComplex_csdLean4 {n : Type} : PosSMulMono ℝ (Matrix n n ℂ)

Nonnegative real scaling is Löwner-monotone (0 ≤ c, A ≤ B ⟹ c • A ≤ c • B). The real scalar action coincides entrywise with the complex one (c • M = (c : ℂ) • M); the complex-scalar Matrix.PosSemidef.smul then applies.

instance Matrix.instSMulPosMonoRealComplex_csdLean4 {n : Type} : SMulPosMono ℝ (Matrix n n ℂ)

Scaling a PSD matrix by a larger real is Löwner-larger (0 ≤ A, c ≤ d ⟹ c • A ≤ d • A).

instance Matrix.instIsOrderedModuleRealComplex_csdLean4 {n : Type} : IsOrderedModule ℝ (Matrix n n ℂ)

Matrix n n ℂ with the Löwner order and Frobenius norm is an ordered ℝ-module.