Nonnegative contractions in a C⋆-algebra form an approximate unit

This file shows that the collection of positive contractions (of norm strictly less than one) in a possibly non-unital C⋆-algebra form a directed set. The key step uses the continuous functional calculus applied with the functions fun x : ℝ≥0, 1 - (1 + x)⁻¹ and fun x : ℝ≥0, x * (1 - x)⁻¹, which are inverses on the interval {x : ℝ≥0 | x < 1}.

In addition, this file defines IsIncreasingApproximateUnit to be a filter l that is an approximate unit contained in the closed unit ball of nonnegative elements. Every C⋆-algebra has a filter generated by the sections {x | a ≤ x} ∩ closedBall 0 1 for 0 ≤ a and ‖a‖ < 1, and moreover, this filter is an increasing approximate unit.

Main declarations

• CFC.monotoneOn_one_sub_one_add_inv: the function f := fun x : ℝ≥0, 1 - (1 + x)⁻¹ is operator monotone on Set.Ici (0 : A) (i.e., cfcₙ f is monotone on {x : A | 0 ≤ x}).
• Set.InvOn.one_sub_one_add_inv: the functions f := fun x : ℝ≥0, 1 - (1 + x)⁻¹ and g := fun x : ℝ≥0, x * (1 - x)⁻¹ are inverses on {x : ℝ≥0 | x < 1}.
• CStarAlgebra.directedOn_nonneg_ball: the set {x : A | 0 ≤ x} ∩ Metric.ball 0 1 is directed.
• Filter.IsIncreasingApproximateUnit: a filter l is an increasing approximate unit if it is an approximate unit contained in the closed unit ball of nonnegative elements.
• CStarAlgebra.approximateUnit: the filter generated by the sections {x | a ≤ x} ∩ closedBall 0 1 for 0 ≤ a with ‖a‖ < 1.
• CStarAlgebra.increasingApproximateUnit: the filter CStarAlgebra.approximateUnit is an increasing approximate unit.

theorem CFC.monotoneOn_one_sub_one_add_inv {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] : MonotoneOn (cfcₙ fun (x : NNReal) => 1 - (1 + x)⁻¹) (Set.Ici 0)

theorem Set.InvOn.one_sub_one_add_inv : Set.InvOn (fun (x : NNReal) => 1 - (1 + x)⁻¹) (fun (x : NNReal) => x * (1 - x)⁻¹) {x : NNReal | x < 1} {x : NNReal | x < 1}

theorem norm_cfcₙ_one_sub_one_add_inv_lt_one {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] (a : A) : ‖cfcₙ (fun (x : NNReal) => 1 - (1 + x)⁻¹) a‖ < 1

theorem CStarAlgebra.directedOn_nonneg_ball {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] : DirectedOn (fun (x1 x2 : A) => x1 ≤ x2) ({x : A | 0 ≤ x} ∩ Metric.ball 0 1)

structure Filter.IsIncreasingApproximateUnit {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] (l : Filter A) extends l.IsApproximateUnit : Prop

An increasing approximate unit in a C⋆-algebra is an approximate unit contained in the closed unit ball of nonnegative elements.

• tendsto_mul_left (m : A) : Filter.Tendsto (fun (x : A) => m * x) l (nhds m)
• tendsto_mul_right (m : A) : Filter.Tendsto (fun (x : A) => x * m) l (nhds m)
• neBot : l.NeBot
• eventually_nonneg : ∀ᶠ (x : A) in l, 0 ≤ x
• eventually_norm : ∀ᶠ (x : A) in l, ‖x‖ ≤ 1

theorem Filter.IsIncreasingApproximateUnit.eventually_nnnorm {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] {l : Filter A} (hl : l.IsIncreasingApproximateUnit) : ∀ᶠ (x : A) in l, ‖x‖₊ ≤ 1

theorem Filter.IsIncreasingApproximateUnit.eventually_isSelfAdjoint {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {l : Filter A} (hl : l.IsIncreasingApproximateUnit) : ∀ᶠ (x : A) in l, IsSelfAdjoint x

theorem Filter.IsIncreasingApproximateUnit.eventually_star_eq {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {l : Filter A} (hl : l.IsIncreasingApproximateUnit) : ∀ᶠ (x : A) in l, star x = x

theorem CStarAlgebra.tendsto_mul_right_of_forall_nonneg_tendsto {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {l : Filter A} (h : ∀ (m : A), 0 ≤ m → ‖m‖ < 1 → Filter.Tendsto (fun (x : A) => x * m) l (nhds m)) (m : A) : Filter.Tendsto (fun (x : A) => x * m) l (nhds m)

To show that l is a one-sided approximate unit for A, it suffices to verify it only for m : A with 0 ≤ m and ‖m‖ < 1.

theorem CStarAlgebra.tendsto_mul_left_iff_tendsto_mul_right {A : Type u_1} [NonUnitalCStarAlgebra A] {l : Filter A} (hl : ∀ᶠ (x : A) in l, IsSelfAdjoint x) : (∀ (m : A), Filter.Tendsto (fun (x : A) => m * x) l (nhds m)) ↔ ∀ (m : A), Filter.Tendsto (fun (x : A) => x * m) l (nhds m)

Multiplication on the left by m tends to 𝓝 m if and only if multiplication on the right does, provided the elements are eventually selfadjoint along the filter l.

theorem CStarAlgebra.isBasis_nonneg_sections (A : Type u_1) [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] : Filter.IsBasis (fun (x : A) => 0 ≤ x ∧ ‖x‖ < 1) fun (x : A) => {x_1 : A | x ≤ x_1}

The sections of positive strict contractions form a filter basis.

def CStarAlgebra.approximateUnit (A : Type u_1) [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] : Filter A

The canonical approximate unit in a C⋆-algebra generated by the basis of sets {x | a ≤ x} ∩ closedBall 0 1 for 0 ≤ a. See also CStarAlgebra.hasBasis_approximateUnit.

Equations

• CStarAlgebra.approximateUnit A = ⋯.filter ⊓ Filter.principal (Metric.closedBall 0 1)

theorem CStarAlgebra.hasBasis_approximateUnit (A : Type u_1) [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] : (CStarAlgebra.approximateUnit A).HasBasis (fun (x : A) => 0 ≤ x ∧ ‖x‖ < 1) fun (x : A) => {x_1 : A | x ≤ x_1} ∩ Metric.closedBall 0 1

The canonical approximate unit in a C⋆-algebra has a basis of sets {x | a ≤ x} ∩ closedBall 0 1 for 0 ≤ a.

theorem CStarAlgebra.nnnorm_sub_mul_self_le {A : Type u_2} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {x y : A} (z : A) (hx₀ : 0 ≤ x) (hy : y ∈ Set.Icc x 1) {c : NNReal} (h : ‖star z * (1 - x) * z‖₊ ≤ c ^ 2) : ‖z - y * z‖₊ ≤ c

This is a common reasoning sequence in C⋆-algebra theory. If 0 ≤ x ≤ y ≤ 1, then the norm of z - y * z is controled by the norm of star z * (1 - x) * z, which is advantageous because the latter is nonnegative. This is a key step in establishing the existence of an increasing approximate unit in general C⋆-algebras.

theorem CStarAlgebra.norm_sub_mul_self_le {A : Type u_2} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {x y : A} (z : A) (hx₀ : 0 ≤ x) (hy : y ∈ Set.Icc x 1) {c : ℝ} (hc : 0 ≤ c) (h : ‖star z * (1 - x) * z‖ ≤ c ^ 2) : ‖z - y * z‖ ≤ c

A variant of nnnorm_sub_mul_self_le which uses ‖·‖ instead of ‖·‖₊.

theorem CStarAlgebra.norm_sub_mul_self_le_of_inr {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {x y : A} (z : A) (hx₀ : 0 ≤ x) (hxy : x ≤ y) (hy₁ : ‖y‖ ≤ 1) {c : ℝ} (hc : 0 ≤ c) (h : ‖star ↑z * (1 - ↑x) * ↑z‖ ≤ c ^ 2) : ‖z - y * z‖ ≤ c

A variant of norm_sub_mul_self_le for non-unital algebras that passes to the unitization.

theorem CStarAlgebra.increasingApproximateUnit (A : Type u_1) [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] : (CStarAlgebra.approximateUnit A).IsIncreasingApproximateUnit

The filter CStarAlgebra.approximateUnit generated by the sections {x | a ≤ x} ∩ closedBall 0 1 for 0 ≤ a forms an increasing approximate unit.