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

This file will show (although it does not yet) that the collection of positive contractions (of norm strictly less than one) in a possibly non-unital C⋆-algebra form an approximate unit. The key step is to show that this set is directed using 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}.

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.

TODO

• Prove the approximate identity result by following Ken Davidson's proof in "C*-Algebras by Example"

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)