LeanOA.CStarAlgebra.IsStarOrtho

structure IsStarOrtho {R : Type u_1} [NonUnitalSemiring R] [StarRing R] (p q : R) :

Two elements p and q in a ⋆-ring are star-orthogonal if star q * p = 0 and p * star q = 0. If p and q are both selfadjoint, this reduces to p * q = 0.

mul_star_eq_zero : p * star q = 0
star_mul_eq_zero : star q * p = 0

Instances For

source

theorem isStarOrtho_iff {R : Type u_1} [NonUnitalSemiring R] [StarRing R] (p q : R) :

IsStarOrtho p q ↔ p * star q = 0 ∧ star q * p = 0

source

def StarRing.«term_⋆⟂_» :

Lean.TrailingParserDescr

Two elements p and q in a ⋆-ring are star-orthogonal if star q * p = 0 and p * star q = 0. If p and q are both selfadjoint, this reduces to p * q = 0.

Equations

StarRing.«term_⋆⟂_» = Lean.ParserDescr.trailingNode `StarRing.«term_⋆⟂_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⋆⟂ ") (Lean.ParserDescr.cat `term 51))

Instances For

source

theorem isStarOrtho_comm {R : Type u_1} [NonUnitalSemiring R] [StarRing R] {p q : R} :

IsStarOrtho p q ↔ IsStarOrtho q p

source

theorem IsStarOrtho.symm {R : Type u_1} [NonUnitalSemiring R] [StarRing R] {p q : R} :

IsStarOrtho p q → IsStarOrtho q p

Alias of the forward direction of isStarOrtho_comm.

source

instance instSymmIsStarOrtho {R : Type u_1} [NonUnitalSemiring R] [StarRing R] :

Std.Symm fun (x1 x2 : R) => IsStarOrtho x1 x2

source

theorem isStarOrtho_iff' {R : Type u_1} [NonUnitalSemiring R] [StarRing R] {p q : R} :

IsStarOrtho p q ↔ p * star q = 0 ∧ star p * q = 0

source

theorem IsStarOrtho.commute {R : Type u_1} [NonUnitalSemiring R] [StarRing R] {p q : R} (h : IsStarOrtho p q) :

Commute p (star q)

source

theorem IsStarOrtho.mul_star_eq_zero' {R : Type u_1} [NonUnitalSemiring R] [StarRing R] {p q : R} (h : IsStarOrtho p q) :

q * star p = 0

The equation IsStarOrtho.mul_star_eq_zero with the roles of p and q interchanged.

source

theorem IsStarOrtho.star_mul_eq_zero' {R : Type u_1} [NonUnitalSemiring R] [StarRing R] {p q : R} (h : IsStarOrtho p q) :

star p * q = 0

The equation IsStarOrtho.star_mul_eq_zero with the roles of p and q interchanged.

source

@[simp]

theorem IsStarOrtho.zero_left {R : Type u_1} [NonUnitalSemiring R] [StarRing R] (q : R) :

IsStarOrtho 0 q

source

@[simp]

theorem IsStarOrtho.zero_right {R : Type u_1} [NonUnitalSemiring R] [StarRing R] (p : R) :

IsStarOrtho p 0

source

theorem IsStarOrtho.star {R : Type u_1} [NonUnitalSemiring R] [StarRing R] {p q : R} (h : IsStarOrtho p q) :

IsStarOrtho (star p) (star q)

source

@[simp]

theorem IsStarOrtho.star_iff {R : Type u_1} [NonUnitalSemiring R] [StarRing R] {p q : R} :

IsStarOrtho (star p) (star q) ↔ IsStarOrtho p q

source

theorem IsStarOrtho.add_left {R : Type u_1} [NonUnitalSemiring R] [StarRing R] {q p₁ p₂ : R} (h₁ : IsStarOrtho p₁ q) (h₂ : IsStarOrtho p₂ q) :

IsStarOrtho (p₁ + p₂) q

source

theorem IsStarOrtho.add_right {R : Type u_1} [NonUnitalSemiring R] [StarRing R] {p q₁ q₂ : R} (h₁ : IsStarOrtho p q₁) (h₂ : IsStarOrtho p q₂) :

IsStarOrtho p (q₁ + q₂)

source

theorem IsStarOrtho.smul_left {R : Type u_1} [NonUnitalSemiring R] [StarRing R] {p q : R} {S : Type u_2} [SMulZeroClass S R] [IsScalarTower S R R] [SMulCommClass S R R] (h : IsStarOrtho p q) (c : S) :

IsStarOrtho (c • p) q

source

theorem IsStarOrtho.smul_right {R : Type u_1} [NonUnitalSemiring R] [StarRing R] {p q : R} {S : Type u_2} [SMulZeroClass S R] [IsScalarTower S R R] [SMulCommClass S R R] (h : IsStarOrtho p q) (c : S) :

IsStarOrtho p (c • q)

source

theorem IsStarOrtho.sum_left {R : Type u_1} [NonUnitalSemiring R] [StarRing R] {q : R} {ι : Type u_2} {s : Finset ι} {f : ι → R} (h : ∀ i ∈ s, IsStarOrtho (f i) q) :

IsStarOrtho (∑ i ∈ s, f i) q

source

theorem IsStarOrtho.sum_right {R : Type u_1} [NonUnitalSemiring R] [StarRing R] {p : R} {ι : Type u_2} {s : Finset ι} {f : ι → R} (h : ∀ i ∈ s, IsStarOrtho p (f i)) :

IsStarOrtho p (∑ i ∈ s, f i)

source

theorem IsStarOrtho.star_right_conjugate {R : Type u_1} [NonUnitalSemiring R] [StarRing R] {p q : R} (h : IsStarOrtho p q) (a b : R) :

IsStarOrtho (p * a * star p) (q * b * star q)

If p and q are star-orthogonal, then so are p * a * star p and q * b * star q.

source

theorem IsStarOrtho.star_left_conjugate {R : Type u_1} [NonUnitalSemiring R] [StarRing R] {p q : R} (h : IsStarOrtho p q) (a b : R) :

IsStarOrtho (star p * a * p) (star q * b * q)

If p and q are star-orthogonal, then so are star p * a * p and star q * b * q.

source

theorem IsStarOrtho.mul_mul' {R : Type u_1} [NonUnitalSemiring R] [StarRing R] {p₁ p₂ q₁ q₂ : R} (h₁ : star q₁ * p₁ = 0) (h₂ : p₂ * star q₂ = 0) (a b : R) :

IsStarOrtho (p₁ * a * p₂) (q₁ * b * q₂)

A version of IsStarOrtho.mul_mul with slightly weaker hypotheses.

source

theorem IsStarOrtho.mul_mul {R : Type u_1} [NonUnitalSemiring R] [StarRing R] {p₁ p₂ q₁ q₂ : R} (h₁ : IsStarOrtho p₁ q₁) (h₂ : IsStarOrtho p₂ q₂) (a b : R) :

IsStarOrtho (p₁ * a * p₂) (q₁ * b * q₂)

source

theorem IsStarOrtho.mul_star_self {R : Type u_1} [NonUnitalSemiring R] [StarRing R] {p q : R} (h : IsStarOrtho p q) :

IsStarOrtho (p * star p) (q * star q)

source

theorem IsStarOrtho.star_mul_self {R : Type u_1} [NonUnitalSemiring R] [StarRing R] {p q : R} (h : IsStarOrtho p q) :

IsStarOrtho (star p * p) (star q * q)

source

theorem IsStarOrtho.map {R : Type u_1} [NonUnitalSemiring R] [StarRing R] {p q : R} {S : Type u_2} {F : Type u_3} [NonUnitalSemiring S] [StarRing S] [FunLike F R S] [NonUnitalRingHomClass F R S] [StarHomClass F R S] (f : F) (h : IsStarOrtho p q) :

IsStarOrtho (f p) (f q)

source

theorem IsStarOrtho.star_add_mul_add {R : Type u_1} [NonUnitalSemiring R] [StarRing R] {p q : R} (h : IsStarOrtho p q) :

star (p + q) * (p + q) = star p * p + star q * q

source

theorem IsStarOrtho.add_mul_star_add {R : Type u_1} [NonUnitalSemiring R] [StarRing R] {p q : R} (h : IsStarOrtho p q) :

(p + q) * star (p + q) = p * star p + q * star q

source

theorem Set.Pairwise.star_sum_mul_sum_of_isStarOrtho {R : Type u_1} [NonUnitalSemiring R] [StarRing R] {ι : Type u_2} {s : Finset ι} {f : ι → R} (h : (↑s).Pairwise (Function.onFun (fun (x1 x2 : R) => IsStarOrtho x1 x2) f)) :

star (∑ i ∈ s, f i) * ∑ i ∈ s, f i = ∑ i ∈ s, star (f i) * f i

source

theorem Set.Pairwise.sum_mul_star_sum_of_isStarOrtho {R : Type u_1} [NonUnitalSemiring R] [StarRing R] {ι : Type u_2} {s : Finset ι} {f : ι → R} (h : (↑s).Pairwise (Function.onFun (fun (x1 x2 : R) => IsStarOrtho x1 x2) f)) :

(∑ i ∈ s, f i) * star (∑ i ∈ s, f i) = ∑ i ∈ s, f i * star (f i)

source

theorem IsSelfAdjoint.isStarOrtho_iff {R : Type u_1} [NonUnitalSemiring R] [StarRing R] {p q : R} (hq : IsSelfAdjoint q) :

IsStarOrtho p q ↔ p * q = 0 ∧ q * p = 0

source

theorem IsSelfAdjoint.isStarOrtho_iff' {R : Type u_1} [NonUnitalSemiring R] [StarRing R] {p q : R} (hp : IsSelfAdjoint p) :

IsStarOrtho p q ↔ p * q = 0 ∧ q * p = 0

source

theorem isStarOrtho_iff_mul_eq_zero {R : Type u_1} [NonUnitalSemiring R] [StarRing R] {p q : R} (hp : IsSelfAdjoint p) (hq : IsSelfAdjoint q) :

IsStarOrtho p q ↔ p * q = 0

Selfadjoint elements are star-orthogonal if and only if their product is zero.

source

theorem IsStarOrtho.mul_eq_zero {R : Type u_1} [NonUnitalSemiring R] [StarRing R] {p q : R} (h : IsStarOrtho p q) (hq : IsSelfAdjoint q) :

p * q = 0

source

theorem IsStarOrtho.mul_eq_zero' {R : Type u_1} [NonUnitalSemiring R] [StarRing R] {p q : R} (h : IsStarOrtho p q) (hq : IsSelfAdjoint q) :

q * p = 0

source

theorem IsStarOrtho.isStarProjection_add {R : Type u_1} [NonUnitalSemiring R] [StarRing R] {p q : R} (h : IsStarOrtho p q) (hp : IsStarProjection p) (hq : IsStarProjection q) :

IsStarProjection (p + q)

The sum of star-orthogonal star projections is a star projection.

source

theorem IsStarProjection.add_iff_isStarOrtho {R : Type u_1} [NonUnitalSemiring R] [StarRing R] {p q : R} [IsCancelAdd R] [HasUniqueDiv R] (hp : IsStarProjection p) (hq : IsStarProjection q) :

IsStarProjection (p + q) ↔ IsStarOrtho p q

The sum of star projections is a star projection if and only if they are star-orthogonal.

source

theorem isStarProjection_sum {R : Type u_1} [NonUnitalSemiring R] [StarRing R] {ι : Type u_2} {s : Finset ι} {f : ι → R} (hf : ∀ i ∈ s, IsStarProjection (f i)) (h : (↑s).Pairwise (Function.onFun (fun (x1 x2 : R) => IsStarOrtho x1 x2) f)) :

IsStarProjection (∑ i ∈ s, f i)

A finite sum of pairwise star-orthogonal star projections is a star projection. The converse holds in a star-ordered ring with proper star. See isStarProjection_sum_iff. The converse is not an immediate corollary of IsStarProjection.add_iff_isStarOrtho because we are not assuming the intermediate sums (i.e., over a subset of s) are star projections.

source

@[simp]

theorem IsStarOrtho.neg_left_iff {R : Type u_1} [NonUnitalRing R] [StarRing R] {p q : R} :

IsStarOrtho (-p) q ↔ IsStarOrtho p q

source

@[simp]

theorem IsStarOrtho.neg_right_iff {R : Type u_1} [NonUnitalRing R] [StarRing R] {p q : R} :

IsStarOrtho p (-q) ↔ IsStarOrtho p q

source

theorem IsStarOrtho.neg_left {R : Type u_1} [NonUnitalRing R] [StarRing R] {p q : R} :

IsStarOrtho p q → IsStarOrtho (-p) q

Alias of the reverse direction of IsStarOrtho.neg_left_iff.

source

theorem IsStarOrtho.of_neg_left {R : Type u_1} [NonUnitalRing R] [StarRing R] {p q : R} :

IsStarOrtho (-p) q → IsStarOrtho p q

Alias of the forward direction of IsStarOrtho.neg_left_iff.

source

theorem IsStarOrtho.of_neg_right {R : Type u_1} [NonUnitalRing R] [StarRing R] {p q : R} :

IsStarOrtho p (-q) → IsStarOrtho p q

Alias of the forward direction of IsStarOrtho.neg_right_iff.

source

theorem IsStarOrtho.neg_right {R : Type u_1} [NonUnitalRing R] [StarRing R] {p q : R} :

IsStarOrtho p q → IsStarOrtho p (-q)

Alias of the reverse direction of IsStarOrtho.neg_right_iff.

source

theorem IsStarOrtho.sub_left {R : Type u_1} [NonUnitalRing R] [StarRing R] {q p₁ p₂ : R} (h₁ : IsStarOrtho p₁ q) (h₂ : IsStarOrtho p₂ q) :

IsStarOrtho (p₁ - p₂) q

source

theorem IsStarOrtho.sub_right {R : Type u_1} [NonUnitalRing R] [StarRing R] {p q₁ q₂ : R} (h₁ : IsStarOrtho p q₁) (h₂ : IsStarOrtho p q₂) :

IsStarOrtho p (q₁ - q₂)

source

@[simp]

theorem isStarOrtho_one_left {R : Type u_1} [Semiring R] [StarRing R] {q : R} :

IsStarOrtho 1 q ↔ q = 0

source

@[simp]

theorem isStarOrtho_one_right {R : Type u_1} [Semiring R] [StarRing R] {p : R} :

IsStarOrtho p 1 ↔ p = 0

source

theorem IsStarOrtho.pow_left {R : Type u_1} [Semiring R] [StarRing R] {p q : R} (h : IsStarOrtho p q) {n : ℕ} (hn : n ≠ 0) :

IsStarOrtho (p ^ n) q

source

theorem IsStarOrtho.pow_right {R : Type u_1} [Semiring R] [StarRing R] {p q : R} (h : IsStarOrtho p q) {n : ℕ} (hn : n ≠ 0) :

IsStarOrtho p (q ^ n)

source

theorem IsStarOrtho.pow_pow {R : Type u_1} [Semiring R] [StarRing R] {p q : R} (h : IsStarOrtho p q) {m n : ℕ} (hm : m ≠ 0) (hn : n ≠ 0) :

IsStarOrtho (p ^ m) (q ^ n)

source

theorem IsStarProjection.isStarOrtho_one_sub {R : Type u_1} [Ring R] [StarRing R] {p : R} (hp : IsStarProjection p) :

IsStarOrtho p (1 - p)

source

theorem IsStarProjection.one_sub_isStarOrtho {R : Type u_1} [Ring R] [StarRing R] {p : R} (hp : IsStarProjection p) :

IsStarOrtho (1 - p) p

source

theorem max_pow_of_nonneg {M₀ : Type u_1} [MonoidWithZero M₀] [LinearOrder M₀] [PosMulMono M₀] [MulPosMono M₀] {a b : M₀} (ha : 0 ≤ a) (hb : 0 ≤ b) (n : ℕ) :

max a b ^ n = max (a ^ n) (b ^ n)

source

theorem min_pow_of_nonneg {M₀ : Type u_1} [MonoidWithZero M₀] [LinearOrder M₀] [PosMulMono M₀] [MulPosMono M₀] {a b : M₀} (ha : 0 ≤ a) (hb : 0 ≤ b) (n : ℕ) :

min a b ^ n = min (a ^ n) (b ^ n)

source

@[simp]

theorem isStarOrtho_self_iff {A : Type u_1} [NonUnitalSemiring A] [StarRing A] [IsProperStar A] (p : A) :

IsStarOrtho p p ↔ p = 0

source

theorem mul_star_eq_zero_of_mul_mul_star_eq_zero {A : Type u_1} [NonUnitalSemiring A] [StarRing A] [PartialOrder A] [StarOrderedRing A] [IsProperStar A] {a c : A} (ha : 0 ≤ a) (h : c * a * star c = 0) :

a * star c = 0

If 0 ≤ a and c * a * star c = 0, then a * star c = 0.

source

theorem isStarOrtho_of_nonneg_iff {A : Type u_1} [NonUnitalSemiring A] [StarRing A] [PartialOrder A] [StarOrderedRing A] [IsProperStar A] {a b : A} (ha : 0 ≤ a) :

IsStarOrtho a b ↔ star b * a * b = 0 ∧ b * a * star b = 0

source

theorem isStarOrtho_of_nonneg_of_isSelfAdjoint_iff {A : Type u_1} [NonUnitalSemiring A] [StarRing A] [PartialOrder A] [StarOrderedRing A] [IsProperStar A] {a b : A} (ha : 0 ≤ a) (hb : IsSelfAdjoint b) :

IsStarOrtho a b ↔ b * a * b = 0

source

theorem IsStarOrtho.of_nonneg {A : Type u_1} [NonUnitalSemiring A] [StarRing A] [PartialOrder A] [StarOrderedRing A] [IsProperStar A] {a b : A} (ha : 0 ≤ a) (h₁ : star b * a * b ≤ 0) (h₂ : b * a * star b ≤ 0) :

IsStarOrtho a b

source

theorem IsStarOrtho.of_le {A : Type u_1} [NonUnitalSemiring A] [StarRing A] [PartialOrder A] [StarOrderedRing A] [IsProperStar A] {a b c : A} (ha : 0 ≤ a) (hab : a ≤ b) (hbc : IsStarOrtho b c) :

IsStarOrtho a c

source

theorem IsStarOrtho.of_add_left {A : Type u_1} [NonUnitalSemiring A] [StarRing A] [PartialOrder A] [StarOrderedRing A] [IsProperStar A] {a b c : A} (ha : 0 ≤ a) (hb : 0 ≤ b) (h : IsStarOrtho (a + b) c) :

IsStarOrtho a c

If 0 ≤ a and 0 ≤ b and (a + b) ⋆⟂ c, then a ⋆⟂ c.

source

theorem IsStarOrtho.of_add_right {A : Type u_1} [NonUnitalSemiring A] [StarRing A] [PartialOrder A] [StarOrderedRing A] [IsProperStar A] {a b c : A} (ha : 0 ≤ a) (hb : 0 ≤ b) (h : IsStarOrtho (a + b) c) :

IsStarOrtho b c

If 0 ≤ a and 0 ≤ b and (a + b) ⋆⟂ c, then b ⋆⟂ c.

source

theorem IsStarOrtho.add_iff {A : Type u_1} [NonUnitalSemiring A] [StarRing A] [PartialOrder A] [StarOrderedRing A] [IsProperStar A] {a b c : A} (ha : 0 ≤ a) (hb : 0 ≤ b) :

IsStarOrtho (a + b) c ↔ IsStarOrtho a c ∧ IsStarOrtho b c

source

theorem IsStarOrtho.sum_iff {A : Type u_1} [NonUnitalSemiring A] [StarRing A] [PartialOrder A] [StarOrderedRing A] [IsProperStar A] {ι : Type u_2} {s : Finset ι} {f : ι → A} {c : A} (hf : ∀ i ∈ s, 0 ≤ f i) :

IsStarOrtho (∑ i ∈ s, f i) c ↔ ∀ j ∈ s, IsStarOrtho (f j) c

source

theorem IsStarOrtho.of_sum {A : Type u_1} [NonUnitalSemiring A] [StarRing A] [PartialOrder A] [StarOrderedRing A] [IsProperStar A] {ι : Type u_2} {s : Finset ι} {f : ι → A} {c : A} (hf : ∀ i ∈ s, 0 ≤ f i) :

IsStarOrtho (∑ i ∈ s, f i) c → ∀ j ∈ s, IsStarOrtho (f j) c

If each f i is nonnegative and (∑ i ∈ s, f i) ⋆⟂ c, then f j ⋆⟂ c for every j ∈ s.

source

theorem isStarProjection_sum_iff {A : Type u_1} [NonUnitalRing A] [StarRing A] [PartialOrder A] [StarOrderedRing A] [IsProperStar A] {ι : Type u_2} {s : Finset ι} {f : ι → A} (hf : ∀ i ∈ s, IsStarProjection (f i)) :

IsStarProjection (∑ i ∈ s, f i) ↔ (↑s).Pairwise (Function.onFun (fun (x1 x2 : A) => IsStarOrtho x1 x2) f)

In a star-ordered ring with proper star (e.g., a C⋆-algebra), a finite sum of star projections is a star projection if and only if they are pairwise star-orthogonal.

source

theorem IsStarOrtho.star_left_of_isStarNormal {A : Type u_1} [NonUnitalSemiring A] [StarRing A] [IsProperStar A] {a b : A} (h : IsStarOrtho a b) (ha : IsStarNormal a) :

IsStarOrtho (star a) b

If a is normal and a ⋆⟂ b, then star a ⋆⟂ b.

source

theorem IsStarOrtho.cfcₙ_complex_left {A : Type u_1} [NonUnitalRing A] [StarRing A] [TopologicalSpace A] [IsSemitopologicalRing A] [T2Space A] {a b : A} [Module ℂ A] [IsScalarTower ℂ A A] [SMulCommClass ℂ A A] [IsProperStar A] [NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal] (f : ℂ → ℂ) (h : IsStarOrtho a b) (ha : IsStarNormal a := by cfc_tac) (hf : ContinuousOn f (quasispectrum ℂ a) := by cfc_cont_tac) (hf0 : f 0 = 0 := by cfc_zero_tac) :

IsStarOrtho (cfcₙ f a) b

If a is normal and a ⋆⟂ b, then cfcₙ f a ⋆⟂ b.

source

theorem IsStarOrtho.cfcₙ_complex_right {A : Type u_1} [NonUnitalRing A] [StarRing A] [TopologicalSpace A] [IsSemitopologicalRing A] [T2Space A] {a b : A} [Module ℂ A] [IsScalarTower ℂ A A] [SMulCommClass ℂ A A] [IsProperStar A] [NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal] (f : ℂ → ℂ) (h : IsStarOrtho a b) (hb : IsStarNormal b := by cfc_tac) (hf : ContinuousOn f (quasispectrum ℂ b) := by cfc_cont_tac) (hf0 : f 0 = 0 := by cfc_zero_tac) :

IsStarOrtho a (cfcₙ f b)

If b is normal and a ⋆⟂ b, then a ⋆⟂ cfcₙ f b.

source

theorem IsStarOrtho.cfcₙ_real_left {A : Type u_1} [NonUnitalRing A] [StarRing A] [TopologicalSpace A] [IsSemitopologicalRing A] [T2Space A] {a b : A} [Module ℝ A] [IsScalarTower ℝ A A] [SMulCommClass ℝ A A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] (f : ℝ → ℝ) (h : IsStarOrtho a b) (ha : IsSelfAdjoint a := by cfc_tac) (hf : ContinuousOn f (quasispectrum ℝ a) := by cfc_cont_tac) (hf0 : f 0 = 0 := by cfc_zero_tac) :

IsStarOrtho (cfcₙ f a) b

If a is selfadjoint and a ⋆⟂ b, then cfcₙ f a ⋆⟂ b.

source

theorem IsStarOrtho.cfcₙ_real_right {A : Type u_1} [NonUnitalRing A] [StarRing A] [TopologicalSpace A] [IsSemitopologicalRing A] [T2Space A] {a b : A} [Module ℝ A] [IsScalarTower ℝ A A] [SMulCommClass ℝ A A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] (f : ℝ → ℝ) (h : IsStarOrtho a b) (hb : IsSelfAdjoint b := by cfc_tac) (hf : ContinuousOn f (quasispectrum ℝ b) := by cfc_cont_tac) (hf0 : f 0 = 0 := by cfc_zero_tac) :

IsStarOrtho a (cfcₙ f b)

If b is selfadjoint and a ⋆⟂ b, then a ⋆⟂ cfcₙ f b.

source

theorem IsStarOrtho.cfcₙ_nnreal_left {A : Type u_1} [NonUnitalRing A] [StarRing A] [TopologicalSpace A] [IsSemitopologicalRing A] [T2Space A] {a b : A} [Module ℝ A] [IsScalarTower ℝ A A] [SMulCommClass ℝ A A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [PartialOrder A] [StarOrderedRing A] [NonnegSpectrumClass ℝ A] (f : NNReal → NNReal) (h : IsStarOrtho a b) (ha : 0 ≤ a := by cfc_tac) (hf : ContinuousOn f (quasispectrum NNReal a) := by cfc_cont_tac) (hf0 : f 0 = 0 := by cfc_zero_tac) :

IsStarOrtho (cfcₙ f a) b

If a is nonnegative and a ⋆⟂ b, then cfcₙ f a ⋆⟂ b.

source

theorem IsStarOrtho.cfcₙ_nnreal_right {A : Type u_1} [NonUnitalRing A] [StarRing A] [TopologicalSpace A] [IsSemitopologicalRing A] [T2Space A] {a b : A} [Module ℝ A] [IsScalarTower ℝ A A] [SMulCommClass ℝ A A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [PartialOrder A] [StarOrderedRing A] [NonnegSpectrumClass ℝ A] (f : NNReal → NNReal) (h : IsStarOrtho a b) (hb : 0 ≤ b := by cfc_tac) (hf : ContinuousOn f (quasispectrum NNReal b) := by cfc_cont_tac) (hf0 : f 0 = 0 := by cfc_zero_tac) :

IsStarOrtho a (cfcₙ f b)

If b is nonnegative and a ⋆⟂ b, then a ⋆⟂ cfcₙ f b.

source

theorem isStarOrtho_sqrt_right_iff {A : Type u_1} [NonUnitalRing A] [StarRing A] [TopologicalSpace A] [IsSemitopologicalRing A] [T2Space A] [Module ℝ A] [IsScalarTower ℝ A A] [SMulCommClass ℝ A A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [PartialOrder A] [StarOrderedRing A] [NonnegSpectrumClass ℝ A] {a b : A} (ha : 0 ≤ a) :

IsStarOrtho b (CFC.sqrt a) ↔ IsStarOrtho b a

source

theorem isStarOrtho_sqrt_left_iff {A : Type u_1} [NonUnitalRing A] [StarRing A] [TopologicalSpace A] [IsSemitopologicalRing A] [T2Space A] [Module ℝ A] [IsScalarTower ℝ A A] [SMulCommClass ℝ A A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [PartialOrder A] [StarOrderedRing A] [NonnegSpectrumClass ℝ A] {a b : A} (ha : 0 ≤ a) :

IsStarOrtho (CFC.sqrt a) b ↔ IsStarOrtho a b

source

theorem IsStarOrtho.of_sqrt_right {A : Type u_1} [NonUnitalRing A] [StarRing A] [TopologicalSpace A] [IsSemitopologicalRing A] [T2Space A] [Module ℝ A] [IsScalarTower ℝ A A] [SMulCommClass ℝ A A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [PartialOrder A] [StarOrderedRing A] [NonnegSpectrumClass ℝ A] {a b : A} (ha : 0 ≤ a) :

IsStarOrtho b (CFC.sqrt a) → IsStarOrtho b a

Alias of the forward direction of isStarOrtho_sqrt_right_iff.

source

theorem IsStarOrtho.sqrt_right {A : Type u_1} [NonUnitalRing A] [StarRing A] [TopologicalSpace A] [IsSemitopologicalRing A] [T2Space A] [Module ℝ A] [IsScalarTower ℝ A A] [SMulCommClass ℝ A A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [PartialOrder A] [StarOrderedRing A] [NonnegSpectrumClass ℝ A] {a b : A} (ha : 0 ≤ a) :

IsStarOrtho b a → IsStarOrtho b (CFC.sqrt a)

Alias of the reverse direction of isStarOrtho_sqrt_right_iff.

source

theorem IsStarOrtho.of_sqrt_left {A : Type u_1} [NonUnitalRing A] [StarRing A] [TopologicalSpace A] [IsSemitopologicalRing A] [T2Space A] [Module ℝ A] [IsScalarTower ℝ A A] [SMulCommClass ℝ A A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [PartialOrder A] [StarOrderedRing A] [NonnegSpectrumClass ℝ A] {a b : A} (ha : 0 ≤ a) :

IsStarOrtho (CFC.sqrt a) b → IsStarOrtho a b

Alias of the forward direction of isStarOrtho_sqrt_left_iff.

source

theorem IsStarOrtho.sqrt_left {A : Type u_1} [NonUnitalRing A] [StarRing A] [TopologicalSpace A] [IsSemitopologicalRing A] [T2Space A] [Module ℝ A] [IsScalarTower ℝ A A] [SMulCommClass ℝ A A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [PartialOrder A] [StarOrderedRing A] [NonnegSpectrumClass ℝ A] {a b : A} (ha : 0 ≤ a) :

IsStarOrtho a b → IsStarOrtho (CFC.sqrt a) b

Alias of the reverse direction of isStarOrtho_sqrt_left_iff.

source

theorem IsStarOrtho.norm_add {A : Type u_1} [NonUnitalCStarAlgebra A] {a b : A} (h : IsStarOrtho a b) :

‖a + b‖ = max ‖a‖ ‖b‖

source

theorem IsStarOrtho.nnnorm_add {A : Type u_1} [NonUnitalCStarAlgebra A] {a b : A} (h : IsStarOrtho a b) :

‖a + b‖₊ = max ‖a‖₊ ‖b‖₊

source

theorem IsStarOrtho.norm_sub {A : Type u_1} [NonUnitalCStarAlgebra A] {a b : A} (h : IsStarOrtho a b) :

‖a - b‖ = max ‖a‖ ‖b‖

source

theorem IsStarOrtho.nnnorm_sub {A : Type u_1} [NonUnitalCStarAlgebra A] {a b : A} (h : IsStarOrtho a b) :

‖a - b‖₊ = max ‖a‖₊ ‖b‖₊

source

theorem IsStarOrtho.nnnorm_sum {A : Type u_1} [NonUnitalCStarAlgebra A] {ι : Type u_2} {s : Finset ι} {f : ι → A} (h : (↑s).Pairwise (Function.onFun (fun (x1 x2 : A) => IsStarOrtho x1 x2) f)) :

‖∑ i ∈ s, f i‖₊ = s.sup fun (x : ι) => ‖f x‖₊