Commit 2024-11-27 03:15 bdc1ed1f

View on Github →

feat: approximate units in C⋆-algebras (#18506) This constructs the canonical approximate unit in an arbitrary C⋆-algebra. This approximate unit is the filter corresponding to the basis of sections {x | a ≤ x} ∩ closedBall 0 1, where 0 ≤ a and ‖a‖ < 1.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/CStarAlgebra/ApproximateUnit.lean

added def CStarAlgebra.approximateUnit

added theorem CStarAlgebra.hasBasis_approximateUnit

added theorem CStarAlgebra.increasingApproximateUnit

added theorem CStarAlgebra.isBasis_nonneg_sections

added theorem CStarAlgebra.nnnorm_sub_mul_self_le

added theorem CStarAlgebra.norm_sub_mul_self_le

added theorem CStarAlgebra.norm_sub_mul_self_le_of_inr

added theorem CStarAlgebra.tendsto_mul_left_iff_tendsto_mul_right

added theorem CStarAlgebra.tendsto_mul_right_of_forall_nonneg_tendsto

added theorem Filter.IsIncreasingApproximateUnit.eventually_isSelfAdjoint

added theorem Filter.IsIncreasingApproximateUnit.eventually_nnnorm

added theorem Filter.IsIncreasingApproximateUnit.eventually_star_eq

added structure Filter.IsIncreasingApproximateUnit

Created Mathlib/Analysis/CStarAlgebra/SpecialFunctions/PosPart.lean

added theorem CStarAlgebra.span_nonneg_inter_ball

added theorem CStarAlgebra.span_nonneg_inter_closedBall

added theorem CStarAlgebra.span_nonneg_inter_unitBall

added theorem CStarAlgebra.span_nonneg_inter_unitClosedBall

Modified Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/PosPart.lean

added theorem CStarAlgebra.linear_combination_nonneg

added theorem CStarAlgebra.span_nonneg