Exact source: MathlibAnnex/Analysis/CStarAlgebra/Representation/DensityLowerBound.lean
Pinned GitHub source · Raw UTF-8 source
Back to Exact norm density of the fixed atomic algebra
1import Mathlib.Tactic.FunProp2import MathlibAnnex.Analysis.CStarAlgebra.Representation.CompactModelDensity3import MathlibAnnex.Analysis.CStarAlgebra.Representation.OrdinarySingleton4import MathlibAnnex.Analysis.CStarAlgebra.NonUnital.DensityLowerBound56/-!7# Unital and ordinary-representation density endpoints89These interfaces specialize the density argument to unital source algebras10while retaining the original quantifier over ordinary nonzero irreducible11representations. The unit need not be explicitly preserved by competitors.12-/1314set_option autoImplicit false1516open Set17open scoped Cardinal ComplexOrder1819namespace MathlibAnnex.Analysis.CStarAlgebra2021universe u v2223variable {A : Type u} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A]24variable {H : Type v} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]2526namespace Representation2728/-- The density version of the ordinary-competitor Rosenberg conclusion. -/29theorem isCompactOperatorModel_of_singleton_amongNonUnital_of_dense30 [Nontrivial A] (pi : Representation A H)31 (hsingle : IsSingletonIrreducibleModelAmongNonUnital.{u, v, u} pi)32 (s : Set H) (hs : Dense s) (hcard : #s < Cardinal.continuum) :33 IsCompactOperatorModel pi.toNonUnitalStarAlgHom :=34 isCompactOperatorModel_of_singleton_of_dense pi hsingle.isSingletonIrreducibleModel s hs hcard3536/-- Dense subsets of an infinite-dimensional unital singleton model cannot37have cardinality below the continuum. -/38theorem continuum_le_cardinalMk_dense_space_of_singleton_of_not_finiteDimensional39 [Nontrivial A] (pi : Representation A H)40 (hsingle : IsSingletonIrreducibleModel.{u, v, u} pi)41 (hA : ¬ FiniteDimensional ℂ A) (s : Set H) (hs : Dense s) :42 Cardinal.continuum ≤ #s := by43 by_contra h44 exact hA (finiteDimensional_algebra_of_singleton_of_dense45 pi hsingle s hs (lt_of_not_ge h))4647/-- A small dense subset of a unital algebra gives a small dense subset of48any nonzero irreducible model by continuity of one nonzero vector's orbit. -/49theorem exists_dense_cardinalMk_lt_continuum_of_isIrreducible50 (pi : Representation A H) (hirr : pi.IsIrreducible)51 (s : Set A) (hs : Dense s) (hcard : #s < Cardinal.continuum) :52 ∃ t : Set H, Dense t ∧ #t < Cardinal.continuum := by53 letI : Nontrivial H := nontrivial_of_isNonzero pi hirr.154 obtain ⟨x, hx⟩ : ∃ x : H, x ≠ 0 := exists_ne 055 have horbit := denseRange_orbitMap_of_isIrreducible pi hirr hx56 have hcont : Continuous (fun a : A => pi a x) := by fun_prop57 exact MathlibAnnex.Topology.exists_dense_cardinalMk_lt_continuum_of_continuous_denseRange58 (fun a : A => pi a x) hcont horbit s hs hcard5960/-- The algebra's norm-density lower bound in the unital infinite-dimensional case. -/61theorem continuum_le_cardinalMk_dense_algebra_of_singleton_of_not_finiteDimensional62 [Nontrivial A] (pi : Representation A H)63 (hsingle : IsSingletonIrreducibleModel.{u, v, u} pi)64 (hA : ¬ FiniteDimensional ℂ A) (s : Set A) (hs : Dense s) :65 Cardinal.continuum ≤ #s := by66 by_contra h67 obtain ⟨t, ht, htcard⟩ := exists_dense_cardinalMk_lt_continuum_of_isIrreducible68 pi hsingle.1 s hs (lt_of_not_ge h)69 exact hA (finiteDimensional_algebra_of_singleton_of_dense pi hsingle t ht htcard)7071/-- The same lower bound with all ordinary possibly nonunital competitors included. -/72theorem continuum_le_cardinalMk_dense_algebra_of_singleton_amongNonUnital_of_not_finiteDimensional73 [Nontrivial A] (pi : Representation A H)74 (hsingle : IsSingletonIrreducibleModelAmongNonUnital.{u, v, u} pi)75 (hA : ¬ FiniteDimensional ℂ A) (s : Set A) (hs : Dense s) :76 Cardinal.continuum ≤ #s :=77 continuum_le_cardinalMk_dense_algebra_of_singleton_of_not_finiteDimensional78 pi hsingle.isSingletonIrreducibleModel hA s hs7980end Representation81end MathlibAnnex.Analysis.CStarAlgebra