Matrix operations on HermitianMats with the CFC

theorem Matrix.IsHermitian.spectrum_subset_Ici_of_sub {d : Type u_1} {𝕜 : Type u_2} [Fintype d] [DecidableEq d] [RCLike 𝕜] {A x : Matrix d d 𝕜} (hA : A.IsHermitian) (hl : (x - A).PosSemidef) : spectrum ℝ x ⊆ Set.Ici (⨅ (i : d), hA.eigenvalues i)

theorem Matrix.IsHermitian.spectrum_subset_Iic_of_sub {d : Type u_1} {𝕜 : Type u_2} [Fintype d] [DecidableEq d] [RCLike 𝕜] {A x : Matrix d d 𝕜} (hA : A.IsHermitian) (hl : (A - x).PosSemidef) : spectrum ℝ x ⊆ Set.Iic (⨆ (i : d), hA.eigenvalues i)

theorem Matrix.IsHermitian.spectrum_subset_of_mem_Icc {d : Type u_1} {𝕜 : Type u_2} [Fintype d] [DecidableEq d] [RCLike 𝕜] {A B x : Matrix d d 𝕜} (hA : A.IsHermitian) (hB : B.IsHermitian) (hl : (x - A).PosSemidef) (hr : (B - x).PosSemidef) : spectrum ℝ x ⊆ Set.Icc (⨅ (i : d), hA.eigenvalues i) (⨆ (i : d), hB.eigenvalues i)

def HermitianMat.termHerm_cont : Lean.ParserDescr

Equations

• HermitianMat.termHerm_cont = Lean.ParserDescr.node `HermitianMat.termHerm_cont 1024 (Lean.ParserDescr.symbol "herm_cont")

@[simp]

theorem HermitianMat.conjTranspose_cfc {d : Type u_1} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [RCLike 𝕜] (A : HermitianMat d 𝕜) (f : ℝ → ℝ) : (_root_.cfc f ↑A).conjTranspose = _root_.cfc f ↑A

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

Equations

• A.cfc f = ⟨cfc f ↑A, ⋯⟩

@[simp]

theorem HermitianMat.cfc_toMat {d : Type u_1} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [RCLike 𝕜] (A : HermitianMat d 𝕜) (f : ℝ → ℝ) : ↑(A.cfc f) = _root_.cfc f ↑A

@[simp]

theorem HermitianMat.cfc_reindex {d : Type u_1} {d₂ : Type u_2} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [Fintype d₂] [DecidableEq d₂] [RCLike 𝕜] (A : HermitianMat d 𝕜) (f : ℝ → ℝ) (e : d ≃ d₂) : (A.reindex e).cfc f = (A.cfc f).reindex e

Reindexing a matrix commutes with applying the CFC.

theorem HermitianMat.inner_eq_trace_mul' {d : Type u_1} {𝕜 : Type u_3} [Fintype d] [RCLike 𝕜] (A B : HermitianMat d 𝕜) : Inner.inner ℝ A B = RCLike.re (↑A * ↑B).trace

@[simp]

theorem HermitianMat.norm_one {d : Type u_1} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [RCLike 𝕜] : ‖1‖ = √↑(Fintype.card d)

theorem HermitianMat.cfc_eigenvalues {d : Type u_1} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [RCLike 𝕜] (f : ℝ → ℝ) (A : HermitianMat d 𝕜) : ∃ (e : d ≃ d), ⋯.eigenvalues = f ∘ ⋯.eigenvalues ∘ ⇑e

theorem HermitianMat.norm_eq_trace_sq {d : Type u_1} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [RCLike 𝕜] (A : HermitianMat d 𝕜) : ↑‖A‖ ^ 2 = (↑A ^ 2).trace

Here we give HermitianMat versions of many cfc theorems, like cfc_id, cfc_sub, cfc_comp, etc. We need these because (as above) HermitianMat.cfc is different from _root_.cfc.

@[simp]

theorem HermitianMat.cfc_id {d : Type u_1} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [RCLike 𝕜] (A : HermitianMat d 𝕜) : A.cfc id = A

@[simp]

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

theorem HermitianMat.cfc_add {d : Type u_1} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [RCLike 𝕜] (A : HermitianMat d 𝕜) (f g : ℝ → ℝ) : A.cfc (f + g) = A.cfc f + A.cfc g

theorem HermitianMat.cfc_sub {d : Type u_1} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [RCLike 𝕜] (A : HermitianMat d 𝕜) (f g : ℝ → ℝ) : A.cfc (f - g) = A.cfc f - A.cfc g

theorem HermitianMat.cfc_neg {d : Type u_1} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [RCLike 𝕜] (A : HermitianMat d 𝕜) (f : ℝ → ℝ) : A.cfc (-f) = -A.cfc f

theorem HermitianMat.coe_cfc_mul {d : Type u_1} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [RCLike 𝕜] (A : HermitianMat d 𝕜) (f g : ℝ → ℝ) : ↑(A.cfc (f * g)) = ↑(A.cfc f) * ↑(A.cfc g)

We don't have a direct analog of cfc_mul, since we can't generally multiply to HermitianMat's to get another one, so the theorem statement wouldn't be well-typed. But, we can say that the matrices are always equal. See cfc_conj for the coe-free analog to multiplication.

theorem HermitianMat.cfc_comp {d : Type u_1} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [RCLike 𝕜] (A : HermitianMat d 𝕜) (f g : ℝ → ℝ) : A.cfc (g ∘ f) = (A.cfc f).cfc g

theorem HermitianMat.cfc_conj {d : Type u_1} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [RCLike 𝕜] (A : HermitianMat d 𝕜) (f g : ℝ → ℝ) : (conj ↑(A.cfc g)) (A.cfc f) = A.cfc (f * g ^ 2)

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

@[simp]

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

@[simp]

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

@[simp]

theorem HermitianMat.cfc_const_mul {d : Type u_1} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [RCLike 𝕜] (A : HermitianMat d 𝕜) (f : ℝ → ℝ) (r : ℝ) : (A.cfc fun (x : ℝ) => r * f x) = r • A.cfc f

@[simp]

theorem HermitianMat.cfc_apply_zero {d : Type u_1} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [RCLike 𝕜] (f : ℝ → ℝ) : cfc 0 f = f 0 • 1

@[simp]

theorem HermitianMat.cfc_apply_one {d : Type u_1} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [RCLike 𝕜] (f : ℝ → ℝ) : cfc 1 f = f 1 • 1

theorem HermitianMat.cfc_congr {d : Type u_1} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [RCLike 𝕜] (A : HermitianMat d 𝕜) {f g : ℝ → ℝ} (hfg : Set.EqOn f g (spectrum ℝ ↑A)) : A.cfc f = A.cfc g

theorem HermitianMat.cfc_congr_of_zero_le {d : Type u_1} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [RCLike 𝕜] {A : HermitianMat d 𝕜} {f g : ℝ → ℝ} (hA : 0 ≤ A) (hfg : Set.EqOn f g (Set.Ici 0)) : A.cfc f = A.cfc g

Version of cfc_congr specialized to PSD matrices.

theorem HermitianMat.cfc_congr_of_posDef {d : Type u_1} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [RCLike 𝕜] {A : HermitianMat d 𝕜} {f g : ℝ → ℝ} (hA : (↑A).PosDef) (hfg : Set.EqOn f g (Set.Ioi 0)) : A.cfc f = A.cfc g

Version of cfc_congr specialized to positive definite matrices.

@[simp]

theorem HermitianMat.cfc_diagonal {d : Type u_1} [Fintype d] [DecidableEq d] (f : ℝ → ℝ) (g : d → ℝ) : (diagonal g).cfc f = diagonal (f ∘ g)

theorem HermitianMat.zero_le_cfc {d : Type u_1} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [RCLike 𝕜] (A : HermitianMat d 𝕜) (f : ℝ → ℝ) : 0 ≤ A.cfc f ↔ ∀ (i : d), 0 ≤ f (⋯.eigenvalues i)

theorem HermitianMat.zero_le_cfc_of_zero_le {d : Type u_1} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [RCLike 𝕜] {A : HermitianMat d 𝕜} {f : ℝ → ℝ} (hA : 0 ≤ A) (hf : ∀ i ≥ 0, 0 ≤ f i) : 0 ≤ A.cfc f

theorem HermitianMat.cfc_PosDef {d : Type u_1} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [RCLike 𝕜] (A : HermitianMat d 𝕜) (f : ℝ → ℝ) : (↑(A.cfc f)).PosDef ↔ ∀ (i : d), 0 < f (⋯.eigenvalues i)

theorem HermitianMat.norm_eq_sum_eigenvalues_sq {d : Type u_1} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [RCLike 𝕜] (A : HermitianMat d 𝕜) : ‖A‖ ^ 2 = ∑ i : d, ⋯.eigenvalues i ^ 2

theorem HermitianMat.lt_smul_of_norm_lt {d : Type u_1} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [RCLike 𝕜] {A : HermitianMat d 𝕜} {r : ℝ} (h : ‖A‖ ≤ r) : A ≤ r • 1

theorem HermitianMat.ball_subset_Icc {d : Type u_1} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [RCLike 𝕜] (A : HermitianMat d 𝕜) (r : ℝ) : Metric.ball A r ⊆ Set.Icc (A - r • 1) (A + r • 1)

theorem HermitianMat.spectrum_subset_of_mem_Icc {d : Type u_1} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [RCLike 𝕜] (A B : HermitianMat d 𝕜) : ∃ (a : ℝ) (b : ℝ), ∀ (x : HermitianMat d 𝕜), A ≤ x ∧ x ≤ B → spectrum ℝ ↑x ⊆ Set.Icc a b

theorem HermitianMat.cfc_continuous {d : Type u_1} [Fintype d] [DecidableEq d] {f : ℝ → ℝ} (hf : Continuous f) : Continuous fun (x : HermitianMat d ℂ) => x.cfc f

def HermitianMat.rpow {d : Type u_1} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [RCLike 𝕜] (A : HermitianMat d 𝕜) (p : ℝ) : 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 p = A.cfc fun (x : ℝ) => x.rpow p

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.pow_eq_rpow {d : Type u_1} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [RCLike 𝕜] (A : HermitianMat d 𝕜) (p : ℝ) : A ^ p = A.rpow p

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

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

@[simp]

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

@[simp]

theorem HermitianMat.reindex_pow {d : Type u_1} {d₂ : Type u_2} [Fintype d] [DecidableEq d] [Fintype d₂] [DecidableEq d₂] (A : HermitianMat d ℂ) (e : d ≃ d₂) (p : ℝ) : A.reindex e ^ p = (A ^ p).reindex e

theorem HermitianMat.coe_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 𝕜} (hA : 0 ≤ A) {p q : ℝ} (hq : q ≠ 0) (hpq : p + 2 * q ≠ 0) : (conj ↑(A ^ q)) (A ^ p) = A ^ (p + 2 * q)

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

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 only defined for positive definite matrices, and the nullspace of the image is exactly the (λ=1)-eigenspace of the original matrix. It coincides with the standard definition if A is positive definite.

Equations

• A.log = A.cfc Real.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