Properties of the matrix logarithm and exponential

In particular, operator monotonicity and concavity of the matrix logarithm. These are proved using inv_antitone, so, first showing that the matrix inverse is operator antitone for positive definite matrices.

theorem Matrix.IsHermitian.log_smul_of_ne_zero {d : Type u_1} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [RCLike 𝕜] {x : ℝ} {A : Matrix d d 𝕜} (hA : A.IsHermitian) (hx : x ≠ 0) : cfc Real.log (x • A) = Real.log x • cfc (fun (x : ℝ) => if x = 0 then 0 else 1) A + cfc Real.log A

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

Matrix exponential of a Hermitian matrix, as given by the continuous functional calculus with Real.exp

Equations

• A.exp = A.cfc Real.exp

theorem Commute.exp_left' {d : Type u_1} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [RCLike 𝕜] {A B : HermitianMat d 𝕜} (hAB : Commute ↑A ↑B) : Commute ↑A.exp ↑B

Primed because Commute.exp_left refers to NormedSpace.exp instead of HermitianMat.exp.

theorem Commute.exp_right' {d : Type u_1} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [RCLike 𝕜] {A B : HermitianMat d 𝕜} (hAB : Commute ↑A ↑B) : Commute ↑A ↑B.exp

Primed because Commute.exp_right refers to NormedSpace.exp instead of HermitianMat.exp.

@[simp]

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

instance HermitianMat.nonSingular_exp {d : Type u_1} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [RCLike 𝕜] (A : HermitianMat d 𝕜) : A.exp.NonSingular

theorem HermitianMat.exp_nonneg {d : Type u_1} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [RCLike 𝕜] (A : HermitianMat d 𝕜) : 0 ≤ A.exp

The matrix exponential of a Hermitian matrix is nonnegative.

theorem HermitianMat.exp_pos {d : Type u_1} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [RCLike 𝕜] [i : Nonempty d] (A : HermitianMat d 𝕜) : 0 < A.exp

The matrix exponential of a Hermitian matrix is strictly positive (Loewner order). Requires Nonempty since over an empty index type every matrix equals zero and 0 < 0 is false.

def HermitianMat.evalHermitianMatExp : Mathlib.Meta.Positivity.PositivityExt

Positivity extension for HermitianMat.exp: always strictly positive if Nonempty d. TODO: We could add a fallback to give nonnegative if Nonempty d is not available, possibly also print a warning. (Users might often not have Nonempty d in context, and they probably want to.)

Equations

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

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

Matrix logarithm (base e) of a Hermitian matrix, as given by the elementwise real logarithm of the diagonal in a diagonalized form, using Real.log

Note that this means that the nullspace of the image includes all of the nullspace of the original matrix. This contrasts to the standard definition, which is typically defined for positive definite matrices, and the nullspace of the image is exactly the (λ=1)-eigenspace of the original matrix. (We also get the (λ=-1)-eigenspace here!)

It coincides with a standard definition if A is positive definite.

Equations

• A.log = A.cfc Real.log

theorem Commute.log_left {d : Type u_1} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [RCLike 𝕜] {A B : HermitianMat d 𝕜} (hAB : Commute ↑A ↑B) : Commute ↑A.log ↑B

theorem Commute.log_right {d : Type u_1} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [RCLike 𝕜] {A B : HermitianMat d 𝕜} (hAB : Commute ↑A ↑B) : Commute ↑A ↑B.log

@[simp]

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

@[simp]

theorem HermitianMat.log_zero {d : Type u_1} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [RCLike 𝕜] : log 0 = 0

@[simp]

theorem HermitianMat.log_one {d : Type u_1} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [RCLike 𝕜] : log 1 = 0

theorem HermitianMat.log_smul_of_pos {d : Type u_1} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [RCLike 𝕜] {x : ℝ} (A : HermitianMat d 𝕜) (hx : x ≠ 0) : (x • A).log = Real.log x • A.supportProj + A.log

theorem HermitianMat.log_smul {d : Type u_1} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [RCLike 𝕜] {A : HermitianMat d 𝕜} {x : ℝ} (hx : x ≠ 0) [A.NonSingular] : (x • A).log = Real.log x • 1 + A.log

theorem HermitianMat.inv_antitone {d : Type u_1} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [RCLike 𝕜] {A B : HermitianMat d 𝕜} (hA : (↑A).PosDef) (h : A ≤ B) : B⁻¹ ≤ A⁻¹

theorem HermitianMat.Real.integral_inv_sub_inv_finite (x T : ℝ) (hx : 0 < x) (hT : 0 < T) : ∫ (t : ℝ) in 0..T, 1 / (1 + t) - 1 / (x + t) = Real.log x + Real.log ((1 + T) / (x + T))

theorem HermitianMat.Real.tendsto_log_div_add_atTop (x : ℝ) : Filter.Tendsto (fun (T : ℝ) => Real.log ((1 + T) / (x + T))) Filter.atTop (nhds 0)

The limit of $\log((1+T)/(x+T))$ as $T \to \infty$ is 0, for $x > 0$.

theorem HermitianMat.logApprox_mono {d : Type u_1} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [RCLike 𝕜] {x y : HermitianMat d 𝕜} (hx : (↑x).PosDef) (hy : (↑y).PosDef) (hxy : x ≤ y) (T : ℝ) (hT : 0 < T) : ∫ (t : ℝ) in 0..T, (1 + t)⁻¹ • 1 - (x + t • 1)⁻¹ ≤ ∫ (t : ℝ) in 0..T, (1 + t)⁻¹ • 1 - (y + t • 1)⁻¹

Monotonicity of the finite integral approximation of the logarithm.

noncomputable def HermitianMat.logApprox {n : Type u_4} {𝕜 : Type u_5} [Fintype n] [DecidableEq n] [RCLike 𝕜] (x : HermitianMat n 𝕜) (T : ℝ) : HermitianMat n 𝕜

Equations

• x.logApprox T = ∫ (t : ℝ) in 0..T, (1 + t)⁻¹ • 1 - (x + t • 1)⁻¹

noncomputable def HermitianMat.scalarLogApprox (T u : ℝ) : ℝ

Equations

• HermitianMat.scalarLogApprox T u = ∫ (t : ℝ) in 0..T, (1 + t)⁻¹ - (u + t)⁻¹

theorem HermitianMat.scalarLogApprox_eq (x T : ℝ) (hx : 0 < x) (hT : 0 < T) : scalarLogApprox T x = Real.log x + Real.log ((1 + T) / (x + T))

theorem HermitianMat.logApprox_eq_cfc_scalar {d : Type u_1} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [RCLike 𝕜] (x : HermitianMat d 𝕜) (hx : (↑x).PosDef) (T : ℝ) (hT : 0 < T) : x.logApprox T = x.cfc (scalarLogApprox T)

The matrix log approximation is the CFC of the scalar log approximation.

theorem HermitianMat.logApprox_eq_log_add_error {d : Type u_1} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [RCLike 𝕜] (x : HermitianMat d 𝕜) (hx : (↑x).PosDef) (T : ℝ) (hT : 0 < T) : x.logApprox T = x.log + x.cfc fun (u : ℝ) => Real.log ((1 + T) / (u + T))

The log approximation is the log plus an error term.

theorem HermitianMat.tendsto_cfc_log_div_add_atTop {d : Type u_1} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [RCLike 𝕜] (x : HermitianMat d 𝕜) : Filter.Tendsto (fun (T : ℝ) => x.cfc fun (u : ℝ) => Real.log ((1 + T) / (u + T))) Filter.atTop (nhds 0)

The error term in the log approximation tends to 0 as T goes to infinity.

theorem HermitianMat.tendsto_logApprox {d : Type u_1} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [RCLike 𝕜] {x : HermitianMat d 𝕜} (hx : (↑x).PosDef) : Filter.Tendsto (fun (T : ℝ) => x.logApprox T) Filter.atTop (nhds x.log)

The log approximation converges to the matrix logarithm.

theorem HermitianMat.posDef_of_posDef_le {d : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] {A B : HermitianMat d 𝕜} (hA : (↑A).PosDef) (hAB : A ≤ B) : (↑B).PosDef

theorem HermitianMat.log_mono {d : Type u_1} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [RCLike 𝕜] {A B : HermitianMat d 𝕜} (hA : (↑A).PosDef) (hAB : A ≤ B) : A.log ≤ B.log

The matrix logarithm is operator monotone.

theorem HermitianMat.le_of_exp_commute {d : Type u_1} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [RCLike 𝕜] {A B : HermitianMat d 𝕜} (hAB₂ : A.exp ≤ B.exp) : A ≤ B

Monotonicity of exp on commuting operators.

theorem HermitianMat.inv_convex {d : Type u_1} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [RCLike 𝕜] {x y : HermitianMat d 𝕜} (hx : (↑x).PosDef) (hy : (↑y).PosDef) ⦃a b : ℝ⦄ (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) : (a • x + b • y)⁻¹ ≤ a • x⁻¹ + b • y⁻¹

The inverse function is operator convex on positive definite matrices.

theorem HermitianMat.inv_shift_convex {d : Type u_1} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [RCLike 𝕜] {x y : HermitianMat d 𝕜} (hx : (↑x).PosDef) (hy : (↑y).PosDef) ⦃a b : ℝ⦄ (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) (t : ℝ) (ht : 0 ≤ t) : (a • x + b • y + t • 1)⁻¹ ≤ a • (x + t • 1)⁻¹ + b • (y + t • 1)⁻¹

The shifted inverse function is operator convex on positive definite matrices.

theorem HermitianMat.integrable_inv_shift {d : Type u_1} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [RCLike 𝕜] {A : HermitianMat d 𝕜} (hA : (↑A).PosDef) (b : ℝ) (hb : 0 ≤ b) : IntervalIntegrable (fun (t : ℝ) => (A + t • 1)⁻¹) MeasureTheory.volume 0 b

Definition of the approximation of the matrix logarithm.

theorem HermitianMat.logApprox_concave {n : Type u_4} {𝕜 : Type u_5} [Fintype n] [DecidableEq n] [RCLike 𝕜] {x y : HermitianMat n 𝕜} (hx : (↑x).PosDef) (hy : (↑y).PosDef) ⦃a b : ℝ⦄ (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) (T : ℝ) (hT : 0 ≤ T) : a • x.logApprox T + b • y.logApprox T ≤ (a • x + b • y).logApprox T

The finite integral approximation of the matrix logarithm is operator concave.

theorem HermitianMat.log_concave {d : Type u_1} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [RCLike 𝕜] {x y : HermitianMat d 𝕜} (hx : (↑x).PosDef) (hy : (↑y).PosDef) ⦃a b : ℝ⦄ (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) : a • x.log + b • y.log ≤ (a • x + b • y).log

The matrix logarithm is operator concave.

theorem HermitianMat.log_kron_diagonal {m : Type u_4} {n : Type u_5} {𝕜 : Type u_6} [Fintype m] [DecidableEq m] [Fintype n] [DecidableEq n] [RCLike 𝕜] {d₁ : m → ℝ} {d₂ : n → ℝ} (h₁ : ∀ (i : m), 0 < d₁ i) (h₂ : ∀ (j : n), 0 < d₂ j) : ((diagonal 𝕜 d₁).kronecker (diagonal 𝕜 d₂)).log = (diagonal 𝕜 d₁).log.kronecker 1 + kronecker 1 (diagonal 𝕜 d₂).log

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

The logarithm of a Hermitian matrix conjugated by a unitary matrix is the conjugate of the logarithm.

theorem HermitianMat.inner_log_smul_of {d : Type u_1} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [RCLike 𝕜] {A B : HermitianMat d 𝕜} [A.NonSingular] {x : ℝ} (hx : x ≠ 0) : inner ℝ (x • A).log B = Real.log x * B.trace + inner ℝ A.log B

theorem HermitianMat.log_kron_diagonal_with_proj {d : Type u_1} {d₂ : Type u_2} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [Fintype d₂] [DecidableEq d₂] [RCLike 𝕜] {f : d → ℝ} {g : d₂ → ℝ} : ((diagonal 𝕜 f).kronecker (diagonal 𝕜 g)).log = (diagonal 𝕜 f).log.kronecker (diagonal 𝕜 g).supportProj + (diagonal 𝕜 f).supportProj.kronecker (diagonal 𝕜 g).log

theorem HermitianMat.log_kron_with_proj {d : Type u_1} {d₂ : Type u_2} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [Fintype d₂] [DecidableEq d₂] [RCLike 𝕜] {A : HermitianMat d 𝕜} {B : HermitianMat d₂ 𝕜} : (A.kronecker B).log = A.log.kronecker B.supportProj + A.supportProj.kronecker B.log

Generalization of HermitianMat.log_kron for possibly singular matrices.

theorem HermitianMat.log_kron {d : Type u_1} {d₂ : Type u_2} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [Fintype d₂] [DecidableEq d₂] [RCLike 𝕜] {A : HermitianMat d 𝕜} {B : HermitianMat d₂ 𝕜} [A.NonSingular] [B.NonSingular] : (A.kronecker B).log = A.log.kronecker 1 + kronecker 1 B.log

The matrix logarithm of the Kronecker product of two nonsingular Hermitian matrices is the sum of the Kronecker products of their logarithms with the identity matrix.