Matrix operations on HermitianMats with the CFC

theorem HermitianMat.isSelfAdjoint {d : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] (A : HermitianMat d 𝕜) : IsSelfAdjoint ↑A

theorem HermitianMat.continuousOn_finite {α : Type u_5} {β : Type u_6} (f : α → β) (S : Set α) [TopologicalSpace α] [TopologicalSpace β] [T1Space α] [Finite ↑S] : ContinuousOn f S

@[simp]

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

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, ⋯⟩

theorem HermitianMat.cfc_eq {d : Type u_1} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [RCLike 𝕜] (A : HermitianMat d 𝕜) (f : ℝ → ℝ) : A.cfc f = ⟨cfc f ↑A, ⋯⟩

@[simp]

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

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

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_nonneg {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.

theorem Commute.cfc_left {d : Type u_1} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [RCLike 𝕜] (f : ℝ → ℝ) {A B : HermitianMat d 𝕜} (hAB : Commute ↑A ↑B) : Commute ↑(A.cfc f) ↑B

theorem Commute.cfc_right {d : Type u_1} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [RCLike 𝕜] (f : ℝ → ℝ) {A B : HermitianMat d 𝕜} (hAB : Commute ↑A ↑B) : Commute ↑A ↑(B.cfc f)

theorem HermitianMat.cfc_commute {d : Type u_1} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [RCLike 𝕜] {A B : HermitianMat d 𝕜} (f g : ℝ → ℝ) (hAB : Commute ↑A ↑B) : Commute ↑(A.cfc f) ↑(B.cfc g)

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

@[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.spectrum_cfc_eq_image {d : Type u_1} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [RCLike 𝕜] (A : HermitianMat d 𝕜) (f : ℝ → ℝ) : spectrum ℝ ↑(A.cfc f) = f '' spectrum ℝ ↑A

theorem HermitianMat.cfc_toMat_eq_sum_smul_proj {d : Type u_1} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [RCLike 𝕜] (A : HermitianMat d 𝕜) (f : ℝ → ℝ) : ↑(A.cfc f) = ∑ i : d, f (⋯.eigenvalues i) • (↑⋯.eigenvectorUnitary * Matrix.single i i 1 * (↑⋯.eigenvectorUnitary).conjTranspose)

Spectral decomposition of A.cfc f as a sum of scaled projections (matrix version).

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

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_add_apply {d : Type u_1} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [RCLike 𝕜] (A : HermitianMat d 𝕜) (f g : ℝ → ℝ) : (A.cfc fun (x : ℝ) => f x + g x) = 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_sub_apply {d : Type u_1} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [RCLike 𝕜] (A : HermitianMat d 𝕜) (f g : ℝ → ℝ) : (A.cfc fun (x : ℝ) => f x - g x) = 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.cfc_neg_apply {d : Type u_1} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [RCLike 𝕜] (A : HermitianMat d 𝕜) (f : ℝ → ℝ) : (A.cfc fun (x : ℝ) => -f x) = -A.cfc f

theorem HermitianMat.mat_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.mat_cfc_mul_apply {d : Type u_1} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [RCLike 𝕜] (A : HermitianMat d 𝕜) (f g : ℝ → ℝ) : ↑(A.cfc fun (x : ℝ) => f x * g x) = ↑(A.cfc f) * ↑(A.cfc g)

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

@[simp]

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

theorem HermitianMat.cfc_conj_unitary {d : Type u_1} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [RCLike 𝕜] (A : HermitianMat d 𝕜) (f : ℝ → ℝ) (U : ↥(Matrix.unitaryGroup d 𝕜)) : ((conj ↑U) A).cfc f = (conj ↑U) (A.cfc f)

@[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 : ℝ → ℝ) : HermitianMat.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 : ℝ → ℝ) : HermitianMat.cfc 1 f = f 1 • 1

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

theorem HermitianMat.cfc_nonneg_iff {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.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.cfc_nonneg_of_nonneg {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

If a rael function preserves nonnegativity, the CFC preserves PSDness.

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

theorem HermitianMat.trace_mul_cfc {d : Type u_1} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [RCLike 𝕜] (A : HermitianMat d 𝕜) (f : ℝ → ℝ) : (↑A * ↑(A.cfc f)).trace = ↑(∑ i : d, ⋯.eigenvalues i * 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

theorem HermitianMat.Matrix.PosDef.spectrum_subset_Ioi {d : Type u_5} {𝕜 : Type u_6} [Fintype d] [DecidableEq d] [RCLike 𝕜] {A : Matrix d d 𝕜} (hA : A.PosDef) : spectrum ℝ A ⊆ Set.Ioi 0

theorem HermitianMat.continuous_cfc_fun {d : Type u_1} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [RCLike 𝕜] {X : Type u_4} [TopologicalSpace X] (A : HermitianMat d 𝕜) {f : X → ℝ → ℝ} (hf : ∀ (i : ℝ), Continuous fun (x : X) => f x i) : Continuous fun (x : X) => A.cfc (f x)

If f is a continuous family of functions parameterized by x, then (fun x => A.cfc (f x)) is also continuous.

theorem HermitianMat.continuousOn_cfc_fun {d : Type u_1} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [RCLike 𝕜] {X : Type u_4} [TopologicalSpace X] (A : HermitianMat d 𝕜) {f : X → ℝ → ℝ} {S : Set X} {T : Set ℝ} (hf : ∀ i ∈ T, ContinuousOn (fun (x : X) => f x i) S) (hA : spectrum ℝ ↑A ⊆ T) : ContinuousOn (fun (x : X) => A.cfc (f x)) S

ContinuousOn variant for when all the matrices (A x) have a spectrum in a set T, and f is continuous on a set S.

theorem HermitianMat.norm_cfc_le_sqrt_card_mul_bound {d : Type u_1} [Fintype d] [DecidableEq d] {A : HermitianMat d ℂ} {f : ℝ → ℝ} {C : ℝ} (hC : 0 ≤ C) (hf : ∀ x ∈ spectrum ℝ ↑A, ‖f x‖ ≤ C) : ‖A.cfc f‖ ≤ √↑(Fintype.card d) * C

Bound the Frobenius norm of a functional calculus application.

theorem HermitianMat.norm_cfc_sub_cfc_le_sqrt_card {d : Type u_1} [Fintype d] [DecidableEq d] {A : HermitianMat d ℂ} {f g : ℝ → ℝ} : ‖A.cfc f - A.cfc g‖ ≤ √↑(Fintype.card d) * ⨆ x ∈ spectrum ℝ ↑A, ‖f x - g x‖

theorem HermitianMat.norm_cfc_sub_le_of_sup_le {d : Type u_1} [Fintype d] [DecidableEq d] {A : HermitianMat d ℂ} {f g : ℝ → ℝ} {T : Set ℝ} {ε : ℝ} (hT : spectrum ℝ ↑A ⊆ T) (hε : 0 ≤ ε) (h_sup : ∀ x ∈ T, ‖f x - g x‖ ≤ ε) : ‖A.cfc f - A.cfc g‖ ≤ √↑(Fintype.card d) * ε

theorem HermitianMat.dist_lt_of_continuous' {X : Type u_5} [TopologicalSpace X] {f : X → ℝ → ℝ} {S : Set X} {T : Set ℝ} (hT : IsCompact T) (hf : ContinuousOn (fun (p : X × ℝ) => f p.1 p.2) (S ×ˢ T)) {x₀ : X} (hx₀ : x₀ ∈ S) {ε : ℝ} (hε : 0 < ε) : ∃ U ∈ nhds x₀, ∀ x ∈ U ∩ S, ∀ t ∈ T, ‖f x t - f x₀ t‖ < ε

If $f$ is jointly continuous on $S \times T$ and $T$ is compact, then $x \mapsto f(x, \cdot)$ is continuous into the space of bounded functions on $T$ with the uniform norm.

theorem HermitianMat.continuousOn_cfc_of_compact {d : Type u_1} [Fintype d] [DecidableEq d] {K : Set ℝ} {g : ℝ → ℝ} (hK : IsCompact K) (hg : ContinuousOn g K) : ContinuousOn (fun (A : HermitianMat d ℂ) => A.cfc g) {A : HermitianMat d ℂ | spectrum ℝ ↑A ⊆ K}

The functional calculus is continuous on matrices with spectrum in a compact set.

theorem HermitianMat.continuous_cfc_joint_compact {X : Type u_5} {d : Type u_6} [TopologicalSpace X] [Fintype d] [DecidableEq d] {f : X → ℝ → ℝ} {A : X → HermitianMat d ℂ} {S : Set X} {T : Set ℝ} (hT : IsCompact T) (hf : ContinuousOn (fun (p : X × ℝ) => f p.1 p.2) (S ×ˢ T)) (hA₁ : ∀ x ∈ S, spectrum ℝ ↑(A x) ⊆ T) (hA₂ : ContinuousOn (fun (x : X) => A x) S) : ContinuousOn (fun (x : X) => (A x).cfc (f x)) S

theorem HermitianMat.eigenvalue_norm_le {d : Type u_1} [Fintype d] [DecidableEq d] (A : HermitianMat d ℂ) (i : d) : |⋯.eigenvalues i| ≤ ‖A‖

theorem HermitianMat.spectrum_subset_closedBall {d : Type u_1} [Fintype d] [DecidableEq d] (A : HermitianMat d ℂ) : spectrum ℝ ↑A ⊆ Metric.closedBall 0 ‖A‖

The spectrum of a HermitianMat is contained in the closed ball of radius ‖A‖ around 0.

theorem HermitianMat.spectrum_subset_of_isOpen {d : Type u_1} [Fintype d] [DecidableEq d] (A₀ : HermitianMat d ℂ) (U : Set ℝ) (hU : IsOpen U) (hAU : spectrum ℝ ↑A₀ ⊆ U) : ∀ᶠ (B : HermitianMat d ℂ) in nhds A₀, spectrum ℝ ↑B ⊆ U

theorem HermitianMat.continuousWithinAt_cfc_of_continuousOn {d : Type u_1} [Fintype d] [DecidableEq d] {T : Set ℝ} {g : ℝ → ℝ} {A₀ : HermitianMat d ℂ} (hg : ContinuousOn g T) (hA₀ : spectrum ℝ ↑A₀ ⊆ T) : ContinuousWithinAt (fun (B : HermitianMat d ℂ) => B.cfc g) {B : HermitianMat d ℂ | spectrum ℝ ↑B ⊆ T} A₀

theorem HermitianMat.dist_lt_of_continuous_spectrum {d : Type u_1} [Fintype d] [DecidableEq d] {X : Type u_5} [TopologicalSpace X] {f : X → ℝ → ℝ} {A : X → HermitianMat d ℂ} {S : Set X} {T : Set ℝ} (hf : ContinuousOn (fun (p : X × ℝ) => f p.1 p.2) (S ×ˢ T)) (hA₁ : ∀ x ∈ S, spectrum ℝ ↑(A x) ⊆ T) (hA₂ : ContinuousOn (fun (x : X) => A x) S) {x₀ : X} (hx₀ : x₀ ∈ S) {ε : ℝ} (hε : 0 < ε) : ∃ U ∈ nhds x₀, ∀ y ∈ U ∩ S, ∀ t ∈ spectrum ℝ ↑(A y), ‖f y t - f x₀ t‖ < ε

theorem HermitianMat.continuous_cfc_joint {X : Type u_5} {d : Type u_6} [TopologicalSpace X] [Fintype d] [DecidableEq d] {f : X → ℝ → ℝ} {A : X → HermitianMat d ℂ} {S : Set X} {T : Set ℝ} (hf : ContinuousOn (fun (p : X × ℝ) => f p.1 p.2) (S ×ˢ T)) (hA₁ : ∀ x ∈ S, spectrum ℝ ↑(A x) ⊆ T) (hA₂ : ContinuousOn (fun (x : X) => A x) S) : ContinuousOn (fun (x : X) => (A x).cfc (f x)) S

theorem HermitianMat.continuousOn_cfc_fun_nonsingular {d : Type u_1} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [RCLike 𝕜] {X : Type u_4} [TopologicalSpace X] (A : HermitianMat d 𝕜) {f : X → ℝ → ℝ} {S : Set X} (hf : ∀ (i : ℝ), i ≠ 0 → ContinuousOn (fun (x : X) => f x i) S) [A.NonSingular] : ContinuousOn (fun (x : X) => A.cfc (f x)) S

Specialization of continuousOn_cfc_fun for nonsingular matrices.

theorem HermitianMat.continuousOn_cfc_fun_nonneg {d : Type u_1} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [RCLike 𝕜] {X : Type u_4} [TopologicalSpace X] (A : HermitianMat d 𝕜) {f : X → ℝ → ℝ} {S : Set X} (hf : ∀ i ≥ 0, ContinuousOn (fun (x : X) => f x i) S) (hA : 0 ≤ A) : ContinuousOn (fun (x : X) => A.cfc (f x)) S

Specialization of continuousOn_cfc_fun for positive semidefinite matrices.

theorem HermitianMat.continuousOn_cfc_fun_posDef {d : Type u_1} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [RCLike 𝕜] {X : Type u_4} [TopologicalSpace X] (A : HermitianMat d 𝕜) {f : X → ℝ → ℝ} {S : Set X} (hf : ∀ i > 0, ContinuousOn (fun (x : X) => f x i) S) (hA : (↑A).PosDef) : ContinuousOn (fun (x : X) => A.cfc (f x)) S

Specialization of continuousOn_cfc_fun for positive definite matrices.

theorem HermitianMat.inv_cfc_eq_cfc_inv {d : Type u_1} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [RCLike 𝕜] {A : HermitianMat d 𝕜} (f : ℝ → ℝ) (hf : ∀ (i : d), f (⋯.eigenvalues i) ≠ 0) : (A.cfc f)⁻¹ = A.cfc fun (u : ℝ) => (f u)⁻¹

The inverse of the CFC is the CFC of the inverse function.

theorem HermitianMat.cfc_inv {d : Type u_1} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [RCLike 𝕜] {A : HermitianMat d 𝕜} [A.NonSingular] : (A.cfc fun (u : ℝ) => u⁻¹) = A⁻¹

theorem HermitianMat.integral_toMat {d : Type u_1} {𝕜 : Type u_3} [Fintype d] [RCLike 𝕜] (A : ℝ → HermitianMat d 𝕜) (T₁ T₂ : ℝ) {μ : MeasureTheory.Measure ℝ} (hA : IntervalIntegrable A μ T₁ T₂) : ↑(∫ (t : ℝ) in T₁..T₂, A t ∂μ) = ∫ (t : ℝ) in T₁..T₂, ↑(A t) ∂μ

The integral of a Hermitian matrix function commutes with toMat.

theorem HermitianMat.intervalIntegrable_sum_smul_const {d : Type u_1} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [RCLike 𝕜] (T₁ T₂ : ℝ) {μ : MeasureTheory.Measure ℝ} (g : ℝ → d → ℝ) (P : d → Matrix d d 𝕜) (hg : ∀ (i : d), IntervalIntegrable (fun (t : ℝ) => g t i) μ T₁ T₂) : IntervalIntegrable (fun (t : ℝ) => ∑ i : d, g t i • P i) μ T₁ T₂

A sum of scaled constant matrices is integrable if the scalar functions are integrable.

theorem HermitianMat.intervalIntegrable_toMat_iff {d : Type u_1} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [RCLike 𝕜] (A : ℝ → HermitianMat d 𝕜) (T₁ T₂ : ℝ) {μ : MeasureTheory.Measure ℝ} : IntervalIntegrable (fun (t : ℝ) => ↑(A t)) μ T₁ T₂ ↔ IntervalIntegrable A μ T₁ T₂

A function to Hermitian matrices is integrable iff its matrix values are integrable.

theorem HermitianMat.integrable_cfc {d : Type u_1} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [RCLike 𝕜] {A : HermitianMat d 𝕜} (T₁ T₂ : ℝ) (f : ℝ → ℝ → ℝ) {μ : MeasureTheory.Measure ℝ} (hf : ∀ (i : d), IntervalIntegrable (fun (t : ℝ) => f t (⋯.eigenvalues i)) μ T₁ T₂) : IntervalIntegrable (fun (t : ℝ) => A.cfc (f t)) μ T₁ T₂

The CFC of an integrable function family is integrable.

theorem HermitianMat.integral_cfc_eq_cfc_integral {d : Type u_1} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [RCLike 𝕜] {A : HermitianMat d 𝕜} (T₁ T₂ : ℝ) {μ : MeasureTheory.Measure ℝ} (f : ℝ → ℝ → ℝ) (hf : ∀ (i : d), IntervalIntegrable (fun (t : ℝ) => f t (⋯.eigenvalues i)) μ T₁ T₂) : ∫ (t : ℝ) in T₁..T₂, A.cfc (f t) ∂μ = A.cfc fun (u : ℝ) => ∫ (t : ℝ) in T₁..T₂, f t u ∂μ

The integral of the CFC is the CFC of the integral.

theorem HermitianMat.cfc_pos_of_pos {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) (hf₂ : 0 ≤ f 0) : 0 < A.cfc f

theorem Commute.exists_HermitianMat_cfc {d : Type u_1} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [RCLike 𝕜] {A B : HermitianMat d 𝕜} (hAB : Commute ↑A ↑B) : ∃ (C : HermitianMat d 𝕜), (∃ (f : ℝ → ℝ), A = C.cfc f) ∧ ∃ (g : ℝ → ℝ), B = C.cfc g

If two matrices A and B commute, then they is a common matrix with which they are both CFCs of. This is a variant of the common theorem that "commuting matrices can be simultaneously diagonalized."

theorem HermitianMat.cfc_le_cfc_of_PosDef {d : Type u_1} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [RCLike 𝕜] (g : ℝ → ℝ) {A : HermitianMat d 𝕜} (f : ℝ → ℝ) (hfg : ∀ (i : ℝ), 0 < i → f i ≤ g i) (hA : (↑A).PosDef) : A.cfc f ≤ A.cfc g

theorem HermitianMat.cfc_le_cfc_of_commute_monoOn {d : Type u_1} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [RCLike 𝕜] {A B : HermitianMat d 𝕜} {f : ℝ → ℝ} (hf : MonotoneOn f (Set.Ioi 0)) (hAB₁ : Commute ↑A ↑B) (hAB₂ : A ≤ B) (hA : (↑A).PosDef) (hB : (↑B).PosDef) : A.cfc f ≤ B.cfc f

theorem HermitianMat.cfc_le_cfc_of_commute {d : Type u_1} {𝕜 : Type u_3} [Fintype d] [DecidableEq d] [RCLike 𝕜] {A B : HermitianMat d 𝕜} (f : ℝ → ℝ) (hf : Monotone f) (hAB₁ : Commute ↑A ↑B) (hAB₂ : A ≤ B) : A.cfc f ≤ B.cfc f

TODO: See above

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

theorem HermitianMat.trace_cfc_eq {d : Type u_1} [Fintype d] [DecidableEq d] (A : HermitianMat d ℂ) (f : ℝ → ℝ) : (A.cfc f).trace = ∑ i : d, f (⋯.eigenvalues i)

The trace of cfc(f, A) equals the sum of f applied to eigenvalues.

theorem HermitianMat.mulVec_eq_zero_iff_inner_eigenvector_zero {d : Type u_1} [Fintype d] [DecidableEq d] (A : HermitianMat d ℂ) (x : EuclideanSpace ℂ d) : (↑A).mulVec x.ofLp = 0 ↔ ∀ (i : d), ⋯.eigenvalues i ≠ 0 → inner ℂ (⋯.eigenvectorBasis i) x = 0

theorem HermitianMat.cfc_mulVec_expansion {d : Type u_1} [Fintype d] [DecidableEq d] (A : HermitianMat d ℂ) (f : ℝ → ℝ) (x : EuclideanSpace ℂ d) : (↑(A.cfc f)).mulVec x.ofLp = (∑ i : d, ↑(f (⋯.eigenvalues i)) • inner ℂ (⋯.eigenvectorBasis i) x • ⋯.eigenvectorBasis i).ofLp

theorem HermitianMat.ker_cfc_le_ker_on_set {d : Type u_1} [Fintype d] [DecidableEq d] {A : HermitianMat d ℂ} {f : ℝ → ℝ} {s : Set ℝ} (hs : spectrum ℝ ↑A ⊆ s) (h : ∀ i ∈ s, f i = 0 → i = 0) : (A.cfc f).ker ≤ A.ker

theorem HermitianMat.ker_cfc_le_ker {d : Type u_1} [Fintype d] [DecidableEq d] {A : HermitianMat d ℂ} {f : ℝ → ℝ} (h : ∀ (i : ℝ), f i = 0 → i = 0) : (A.cfc f).ker ≤ A.ker

theorem HermitianMat.ker_cfc_le_ker_nonneg {d : Type u_1} [Fintype d] [DecidableEq d] {A : HermitianMat d ℂ} {f : ℝ → ℝ} (hA : 0 ≤ A) (h : ∀ i ≥ 0, f i = 0 → i = 0) : (A.cfc f).ker ≤ A.ker

theorem HermitianMat.ker_le_ker_cfc_on_set {d : Type u_1} [Fintype d] [DecidableEq d] {A : HermitianMat d ℂ} {f : ℝ → ℝ} {s : Set ℝ} (hs : spectrum ℝ ↑A ⊆ s) (h : ∀ i ∈ s, i = 0 → f i = 0) : A.ker ≤ (A.cfc f).ker

theorem HermitianMat.ker_le_ker_cfc {d : Type u_1} [Fintype d] [DecidableEq d] {A : HermitianMat d ℂ} {f : ℝ → ℝ} (h : ∀ (i : ℝ), i = 0 → f i = 0) : A.ker ≤ (A.cfc f).ker

theorem HermitianMat.ker_le_ker_cfc_nonneg {d : Type u_1} [Fintype d] [DecidableEq d] {A : HermitianMat d ℂ} {f : ℝ → ℝ} (hA : 0 ≤ A) (h : ∀ i ≥ 0, i = 0 → f i = 0) : A.ker ≤ (A.cfc f).ker

theorem HermitianMat.ker_cfc_eq_ker {d : Type u_1} [Fintype d] [DecidableEq d] {A : HermitianMat d ℂ} {f : ℝ → ℝ} (h : ∀ (i : ℝ), f i = 0 ↔ i = 0) : (A.cfc f).ker = A.ker

theorem HermitianMat.ker_cfc_eq_ker_nonneg {d : Type u_1} [Fintype d] [DecidableEq d] {A : HermitianMat d ℂ} {f : ℝ → ℝ} (hA : 0 ≤ A) (h : ∀ i ≥ 0, f i = 0 ↔ i = 0) : (A.cfc f).ker = A.ker