Matrix powers with real exponents

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

Matrix power of a positive semidefinite matrix, as given by the elementwise real power of the diagonal in a diagonalized form.

Note that this has the usual Real.rpow caveats, such as 0 to the power -1 giving 0.

Equations

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

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} [Fintype d] [DecidableEq d] (A : HermitianMat d ℂ) (hA : 0 ≤ A) (p : ℝ) (hp : 0 < p) : ((A ^ 2).cfc fun (x : ℝ) => x ^ (p / 2)) = A.cfc fun (x : ℝ) => x ^ 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

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

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.

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

An inequality of Lieb-Thirring type. For 0 < r ≤ 1: Tr[B^r A^r B^r] ≤ Tr[(B A B)^r].

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