Matrix Powers With Real Exponents

This file defines real powers of finite-dimensional Hermitian matrices by continuous functional calculus:

A ^ r = A.cfc (fun x => x ^ r).

The scalar function is Real.rpow, so this is a total operation on Hermitian matrices. For positive semidefinite matrices it has the expected spectral meaning. For negative exponents on singular matrices it follows the Real.rpow convention, so zero eigenvalues remain zero; use positive-definiteness hypotheses for inverse laws.

Main results:

• algebraic and spectral lemmas for real powers;
• continuity in the exponent and in the matrix argument;
• the Loewner-Heinz monotonicity theorem for 0 < q <= 1;
• Lieb-Thirring and Rotfel'd trace inequalities for 0 < p <= 1.

noncomputable def HermitianMat.rpow {d : Type u_1} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [RCLike 𝕜] (A : HermitianMat d 𝕜) (r : ℝ) : HermitianMat d 𝕜

Real powers of Hermitian matrices via continuous functional calculus.

This is the total functional-calculus definition A.cfc (fun x => x ^ r). For positive semidefinite A, this is the usual spectral power. For negative exponents on singular matrices, zero eigenvalues stay zero because this uses Real.rpow.

Equations

• A.rpow r = A.cfc fun (x : ℝ) => x.rpow r

@[implicit_reducible]

noncomputable instance HermitianMat.instRPow {d : Type u_1} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [RCLike 𝕜] : Pow (HermitianMat d 𝕜) ℝ

Equations

• HermitianMat.instRPow = { pow := HermitianMat.rpow }

theorem HermitianMat.rpow_conj_unitary {d : Type u_1} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [RCLike 𝕜] (A : HermitianMat d 𝕜) (U : ↥(Matrix.unitaryGroup d 𝕜)) (r : ℝ) : (conj ↑U) A ^ r = (conj ↑U) (A ^ r)

theorem HermitianMat.pow_eq_rpow {d : Type u_1} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [RCLike 𝕜] {A : HermitianMat d 𝕜} {r : ℝ} : A ^ r = A.rpow r

theorem HermitianMat.rpow_eq_cfc {d : Type u_1} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [RCLike 𝕜] {A : HermitianMat d 𝕜} {r : ℝ} : A ^ r = A.cfc fun (x : ℝ) => x ^ r

theorem HermitianMat.diagonal_pow {d : Type u_1} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [RCLike 𝕜] {r : ℝ} (f : d → ℝ) : diagonal 𝕜 f ^ r = diagonal 𝕜 fun (i : d) => f i ^ r

theorem HermitianMat.rpow_const_continuous {d : Type u_1} [Fintype d] [DecidableEq d] {r : ℝ} (hr : 0 ≤ r) : Continuous fun (A : HermitianMat d ℂ) => A ^ r

theorem HermitianMat.const_rpow_continuous {d : Type u_1} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [RCLike 𝕜] {A : HermitianMat d 𝕜} [A.NonSingular] : Continuous fun (r : ℝ) => A ^ r

theorem HermitianMat.continuousOn_rpow_pos {d : Type u_1} [Fintype d] [DecidableEq d] (A : HermitianMat d ℂ) : ContinuousOn (fun (x : ℝ) => A ^ x) (Set.Ioi 0)

For a fixed Hermitian matrix A, the function x ↦ A^x is continuous for x > 0.

theorem HermitianMat.continuousOn_rpow_neg {d : Type u_1} [Fintype d] [DecidableEq d] (A : HermitianMat d ℂ) : ContinuousOn (fun (x : ℝ) => A ^ x) (Set.Iio 0)

For a fixed Hermitian matrix A, the function x ↦ A^x is continuous for x < 0.

@[simp]

theorem HermitianMat.rpow_one {d : Type u_1} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [RCLike 𝕜] {A : HermitianMat d 𝕜} : A ^ 1 = A

theorem HermitianMat.sqrt_eq_cfc_rpow_half {d : Type u_1} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [RCLike 𝕜] (A : HermitianMat d 𝕜) : A.sqrt = A.cfc fun (x : ℝ) => x ^ (1 / 2)

Functional calculus of Real.sqrt is equal to functional calculus of x^(1/2).

@[simp]

theorem HermitianMat.one_rpow {d : Type u_1} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [RCLike 𝕜] {r : ℝ} : 1 ^ r = 1

@[simp]

theorem HermitianMat.rpow_zero {d : Type u_1} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [RCLike 𝕜] (A : HermitianMat d 𝕜) : A ^ 0 = 1

theorem HermitianMat.rpow_diagonal {d : Type u_1} [Fintype d] [DecidableEq d] (a : d → ℝ) (r : ℝ) : diagonal ℂ a ^ r = diagonal ℂ fun (i : d) => a i ^ r

@[simp]

theorem HermitianMat.reindex_rpow {d : Type u_1} {d₂ : Type u_2} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [Fintype d₂] [DecidableEq d₂] [RCLike 𝕜] {A : HermitianMat d 𝕜} {r : ℝ} (e : d ≃ d₂) : A.reindex e ^ r = (A ^ r).reindex e

Keeps in line with our simp-normal form for moving reindex outwards.

theorem HermitianMat.mat_rpow_add {d : Type u_1} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [RCLike 𝕜] {A : HermitianMat d 𝕜} (hA : 0 ≤ A) {p q : ℝ} (hpq : p + q ≠ 0) : ↑(A ^ (p + q)) = ↑(A ^ p) * ↑(A ^ q)

theorem HermitianMat.rpow_mul {d : Type u_1} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [RCLike 𝕜] {A : HermitianMat d 𝕜} (hA : 0 ≤ A) {p q : ℝ} : A ^ (p * q) = (A ^ p) ^ q

theorem HermitianMat.conj_rpow {d : Type u_1} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [RCLike 𝕜] {A : HermitianMat d 𝕜} {q r : ℝ} (hA : 0 ≤ A) (hq : q ≠ 0) (hqr : r + 2 * q ≠ 0) : (conj ↑(A ^ q)) (A ^ r) = A ^ (r + 2 * q)

theorem HermitianMat.pow_half_mul {d : Type u_1} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [RCLike 𝕜] {A : HermitianMat d 𝕜} (hA : 0 ≤ A) : ↑(A ^ (1 / 2)) * ↑(A ^ (1 / 2)) = ↑A

theorem HermitianMat.rpow_pos {d : Type u_1} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [RCLike 𝕜] {A : HermitianMat d 𝕜} (hA : 0 < A) {p : ℝ} : 0 < A ^ p

theorem HermitianMat.rpow_nonneg {d : Type u_1} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [RCLike 𝕜] {A : HermitianMat d 𝕜} (hA : 0 ≤ A) {p : ℝ} : 0 ≤ A ^ p

theorem HermitianMat.inv_eq_rpow_neg_one {d : Type u_1} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [RCLike 𝕜] {A : HermitianMat d 𝕜} (hA : (↑A).PosDef) : A⁻¹ = A ^ (-1)

theorem HermitianMat.sandwich_self {d : Type u_1} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [RCLike 𝕜] {B : HermitianMat d 𝕜} (hB : (↑B).PosDef) : (conj ↑(B ^ (-1 / 2))) B = 1

theorem HermitianMat.rpow_inv_eq_neg_rpow {d : Type u_1} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [RCLike 𝕜] {A : HermitianMat d 𝕜} (hA : (↑A).PosDef) (p : ℝ) : (A ^ p)⁻¹ = A ^ (-p)

theorem HermitianMat.sandwich_le_one {d : Type u_1} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [RCLike 𝕜] {A B : HermitianMat d 𝕜} (hB : (↑B).PosDef) (h : A ≤ B) : (conj ↑(B ^ (-1 / 2))) A ≤ 1

theorem HermitianMat.rpow_neg_mul_rpow_self {d : Type u_1} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [RCLike 𝕜] {A : HermitianMat d 𝕜} (hA : (↑A).PosDef) (p : ℝ) : ↑(A ^ (-p)) * ↑(A ^ p) = 1

theorem HermitianMat.isUnit_rpow_toMat {d : Type u_1} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [RCLike 𝕜] {A : HermitianMat d 𝕜} (hA : (↑A).PosDef) (p : ℝ) : IsUnit ↑(A ^ p)

theorem HermitianMat.sandwich_inv {d : Type u_1} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [RCLike 𝕜] {A B : HermitianMat d 𝕜} (hB : (↑B).PosDef) : ((conj ↑(B ^ (-1 / 2))) A)⁻¹ = (conj ↑(B ^ (1 / 2))) A⁻¹

theorem HermitianMat.ker_rpow_eq_of_nonneg {d : Type u_1} [Fintype d] [DecidableEq d] {r : ℝ} {A : HermitianMat d ℂ} (hA : 0 ≤ A) (hp : r ≠ 0) : (A ^ r).ker = A.ker

theorem HermitianMat.ker_rpow_le_of_nonneg {d : Type u_1} [Fintype d] [DecidableEq d] {r : ℝ} {A : HermitianMat d ℂ} (hA : 0 ≤ A) : (A ^ r).ker ≤ A.ker

theorem HermitianMat.conj_kron {d : Type u_1} {d₂ : Type u_2} {𝕜 : Type u_3} [Fintype d] [Fintype d₂] [RCLike 𝕜] (A : Matrix d d 𝕜) (B : Matrix d₂ d₂ 𝕜) (C : HermitianMat d 𝕜) (D : HermitianMat d₂ 𝕜) : (conj (Matrix.kroneckerMap (fun (x1 x2 : 𝕜) => x1 * x2) A B)) (C.kronecker D) = ((conj A) C).kronecker ((conj B) D)

theorem HermitianMat.rpow_kron {d : Type u_1} {d₂ : Type u_2} [Fintype d] [DecidableEq d] [Fintype d₂] [DecidableEq d₂] {A : HermitianMat d ℂ} {B : HermitianMat d₂ ℂ} (r : ℝ) (hA : 0 ≤ A) (hB : 0 ≤ B) : A.kronecker B ^ r = (A ^ r).kronecker (B ^ r)

theorem HermitianMat.continuousOn_rpow_uniform {K : Set ℝ} (hK : IsCompact K) : ContinuousOn (fun (r : ℝ) => (UniformOnFun.ofFun {K}) fun (t : ℝ) => t ^ r) (Set.Ioi 0)

theorem HermitianMat.continuousOn_rpow_joint_nonneg_pos {d : Type u_1} [Fintype d] [DecidableEq d] {X : Type u_4} [TopologicalSpace X] {A : X → HermitianMat d ℂ} {p : X → ℝ} {S : Set X} (hA : ContinuousOn A S) (hp : ContinuousOn p S) (hp_pos : ∀ x ∈ S, 0 < p x) : ContinuousOn (fun (x : X) => A x ^ p x) S

Joint continuity of matrix rpow for Hermitian matrices with positive exponent

theorem HermitianMat.cfc_sq_rpow_eq_cfc_rpow {d : Type u_1} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [RCLike 𝕜] (A : HermitianMat d 𝕜) (hA : 0 ≤ A) (p : ℝ) (hp : 0 ≤ p) : ((A ^ 2).cfc fun (x : ℝ) => x ^ (p / 2)) = A.cfc fun (x : ℝ) => x ^ p

For positive semidefinite A, (A ^ 2) ^ (p / 2) = A ^ p in functional calculus form.

The nonnegative exponent assumption is needed for continuity at zero. For positive definite matrices, the same identity should hold for all real p.

theorem HermitianMat.trace_rpow_eq_sum {d : Type u_1} [Fintype d] [DecidableEq d] (A : HermitianMat d ℂ) (p : ℝ) : (A ^ p).trace = ∑ i : d, ⋯.eigenvalues i ^ p

Tr[A^p] = ∑ᵢ λᵢ^p for a Hermitian matrix A.

Loewner-Heinz Theorem

The operator monotonicity of x ↦ x ^ q for 0 < q ≤ 1: if A ≤ B (in the Loewner order), then A ^ q ≤ B ^ q. This is proved using the resolvent integral representation, following the same approach as log_mono in LogExp.lean. The key identity is: x ^ q = c_q * ∫ t in (0,∞), t ^ (q-1) * x / (x + t) dt where c_q = sin(π q) / π. Since each integrand x / (x + t) is operator monotone (via inv_antitone), the integral is operator monotone.

noncomputable def HermitianMat.rpowApprox {d : Type u_1} [Fintype d] [DecidableEq d] (A : HermitianMat d ℂ) (q T : ℝ) : HermitianMat d ℂ

Finite integral approximation for the rpow monotonicity proof. Same integrand as logApprox but with weight t ^ q.

Equations

• A.rpowApprox q T = ∫ (t : ℝ) in 0..T, t ^ q • ((1 + t)⁻¹ • 1 - (A + t • 1)⁻¹)

theorem HermitianMat.rpowApprox_mono {d : Type u_1} [Fintype d] [DecidableEq d] {q : ℝ} {A B : HermitianMat d ℂ} (hA : (↑A).PosDef) (hB : (↑B).PosDef) (hAB : A ≤ B) (hq : 0 ≤ q) (T : ℝ) (hT : 0 < T) : A.rpowApprox q T ≤ B.rpowApprox q T

noncomputable def HermitianMat.scalarRpowApprox (q T x : ℝ) : ℝ

The scalar function underlying rpowApprox via the CFC.

Equations

• HermitianMat.scalarRpowApprox q T x = ∫ (t : ℝ) in 0..T, t ^ q * (1 / (1 + t) - 1 / (x + t))

theorem HermitianMat.rpowApprox_eq_cfc_scalar {d : Type u_1} [Fintype d] [DecidableEq d] (A : HermitianMat d ℂ) (hA : (↑A).PosDef) (q T : ℝ) (hq : 0 ≤ q) (hT : 0 < T) : A.rpowApprox q T = A.cfc (scalarRpowApprox q T)

noncomputable def HermitianMat.rpowConst (q : ℝ) : ℝ

The positive constant arising from the resolvent integral. Equal to ∫ u in Set.Ioi 0, u ^ (q-1) / (1+u) = π / sin(π q), but we only need its positivity.

Equations

• HermitianMat.rpowConst q = ∫ (u : ℝ) in Set.Ioi 0, u ^ (q - 1) / (1 + u)

theorem HermitianMat.rpowConst_integrableOn {q : ℝ} (hq : 0 < q) (hq1 : q < 1) : MeasureTheory.IntegrableOn (fun (u : ℝ) => u ^ (q - 1) / (1 + u)) (Set.Ioi 0) MeasureTheory.volume

The integrand u ^ (q-1) / (1+u) is integrable on (0, ∞) for 0 < q < 1.

theorem HermitianMat.rpowConst_pos {q : ℝ} (hq : 0 < q) (hq1 : q < 1) : 0 < rpowConst q

The resolvent constant is positive for 0 < q < 1.

theorem HermitianMat.scalarRpowApprox_tendsto {q x : ℝ} (hx : 0 < x) (hq : 0 < q) (hq1 : q < 1) : Filter.Tendsto (fun (T : ℝ) => scalarRpowApprox q T x) Filter.atTop (nhds (rpowConst q * (x ^ q - 1)))

The scalar rpow approximation converges pointwise. scalarRpowApprox q T x → rpowConst q * (x^q - 1) as T → ∞.

theorem HermitianMat.tendsto_rpowApprox {d : Type u_1} [Fintype d] [DecidableEq d] {A : HermitianMat d ℂ} {q : ℝ} (hA : (↑A).PosDef) (hq : 0 < q) (hq1 : q < 1) : Filter.Tendsto (A.rpowApprox q) Filter.atTop (nhds (rpowConst q • (A ^ q - 1)))

The matrix rpow approximation converges: rpowApprox A q T → rpowConst q • (A^q - 1).

theorem HermitianMat.rpow_le_rpow_of_posDef {d : Type u_1} [Fintype d] [DecidableEq d] {A B : HermitianMat d ℂ} {q : ℝ} (hA : (↑A).PosDef) (hAB : A ≤ B) (hq : 0 < q) (hq1 : q ≤ 1) : A ^ q ≤ B ^ q

Loewner-Heinz for positive definite lower endpoint.

This is the positive-definite core used to prove the positive-semidefinite statement by adding ε • 1 and taking a limit.

theorem HermitianMat.rpow_le_rpow_of_le {d : Type u_1} [Fintype d] [DecidableEq d] {A B : HermitianMat d ℂ} {q : ℝ} (hA : 0 ≤ A) (hAB : A ≤ B) (hq : 0 < q) (hq1 : q ≤ 1) : A ^ q ≤ B ^ q

The Löwner—Heinz theorem: for matrices A and B, if 0 ≤ A ≤ B and 0 < q ≤ 1, then A^q ≤ B^q. That is, real roots are operator monotone.

Araki-Lieb-Thirring Inequality

The next section proves the trace inequality Tr[(B ^ r) (A ^ r) (B ^ r)] <= Tr[(B A B) ^ r] for 0 < r <= 1. The proof uses compound matrices to convert the multiplicative singular-value estimates into a weak log-majorization argument.

theorem HermitianMat.lieb_thirring_le_one {d : Type u_1} [Fintype d] [DecidableEq d] {A B : HermitianMat d ℂ} (hA : 0 ≤ A) (hB : 0 ≤ B) {r : ℝ} (hr0 : 0 < r) (hr1 : r ≤ 1) : ((conj ↑(B ^ r)) (A ^ r)).trace ≤ ((conj ↑B) A ^ r).trace

Lieb-Thirring type inequality for positive semidefinite Hermitian matrices.

For 0 < r <= 1, Tr[(B ^ r) (A ^ r) (B ^ r)] <= Tr[(B A B) ^ r], written using HermitianMat.conj.

Rotfel'd Trace Subadditivity

For positive semidefinite A, B and 0 < p <= 1, Rotfel'd's inequality says Tr[(A + B) ^ p] <= Tr[A ^ p] + Tr[B ^ p].

The proof here uses the same resolvent-integral representation as Loewner-Heinz, plus monotonicity of the trace after inserting square roots. A stronger version can be stated as a majorization theorem.

theorem HermitianMat.trace_rpow_add_le {d : Type u_1} [Fintype d] [DecidableEq d] {A B : HermitianMat d ℂ} (hA : 0 ≤ A) (hB : 0 ≤ B) (p : ℝ) (hp : 0 < p) (hp1 : p ≤ 1) : ((A + B) ^ p).trace ≤ (A ^ p).trace + (B ^ p).trace

Rotfel'd trace subadditivity for positive semidefinite Hermitian matrices.

For 0 < p <= 1, Tr[(A + B) ^ p] <= Tr[A ^ p] + Tr[B ^ p].