Exact source view. Private integrated preview.
Exact declaration: MathlibAnnex.CStarAlgebra.CAR.hasDensityCharacter_atomicCounterexampleHilbert
MathlibAnnex/Analysis/CStarAlgebra/CAR/Cardinality.lean · lines 69–88
1import MathlibAnnex.Analysis.CStarAlgebra.CAR.SeparableFaithful 2import MathlibAnnex.Analysis.CStarAlgebra.Representation.SeparableCardinality 3import MathlibAnnex.Analysis.CStarAlgebra.Representation.DensityLowerBound 4import MathlibAnnex.Analysis.CStarAlgebra.Representation.DensityCharacter 5 6/-! 7# Cardinality and norm density of the fixed atomic counterexample 8 9The upper bound comes from the already constructed faithful separable model. 10The lower bound applies to every norm-dense subset of this same algebra. 11The whole-carrier cardinality and norm density are distinguished throughout. 12-/ 13set_option autoImplicit false 14open Set 15open scoped Cardinal ComplexOrder 16namespace MathlibAnnex.CStarAlgebra.CAR 17open MathlibAnnex.Analysis.CStarAlgebra MathlibAnnex.Topology 18 19/-- The existing faithful separable representation bounds the fixed carrier. -/ 20theorem cardinalMk_atomicCounterexampleAlgebra_le_continuum : 21 #AtomicCounterexampleAlgebra ≤ Cardinal.continuum := by 22 letI : TopologicalSpace.SeparableSpace SeparableCounterexampleHilbertSpace := 23 separableSpace_separableCounterexampleHilbertSpace 24 exact Representation.cardinalMk_le_continuum_of_injective 25 separableCounterexampleRepresentation separableCounterexampleRepresentation_injective 26 27/-- No norm-dense subset of the fixed algebra is smaller than the continuum. -/ 28theorem continuum_le_cardinalMk_dense_atomicCounterexampleAlgebra 29 (s : Set AtomicCounterexampleAlgebra) (hs : Dense s) : 30 Cardinal.continuum ≤ #s := 31 Representation.continuum_le_cardinalMk_dense_algebra_of_singleton_of_not_finiteDimensional 32 (shellFamilyInclusion homogeneityShellFamily) 33 (isUniqueIrreducibleModel_shellFamilyInclusion.{0} homogeneityShellFamily).2 34 (not_finiteDimensional_shellFamilyTarget homogeneityShellFamily) s hs 35 36/-- The cardinality of the underlying set of the fixed algebra is continuum. -/ 37theorem cardinalMk_atomicCounterexampleAlgebra : 38 #AtomicCounterexampleAlgebra = Cardinal.continuum := by 39 apply le_antisymm cardinalMk_atomicCounterexampleAlgebra_le_continuum 40 simpa using continuum_le_cardinalMk_dense_atomicCounterexampleAlgebra Set.univ dense_univ 41 42/-- The exact norm density of the same fixed algebra is continuum. -/ 43theorem hasDensityCharacter_atomicCounterexampleAlgebra : 44 HasDensityCharacter AtomicCounterexampleAlgebra Cardinal.continuum := 45 HasDensityCharacter.of_cardinalMk_le_of_forall_dense 46 cardinalMk_atomicCounterexampleAlgebra_le_continuum 47 continuum_le_cardinalMk_dense_atomicCounterexampleAlgebra 48 49/-- Under CH, the fixed algebra has exact norm density aleph one. CH is an 50explicit premise, not an added axiom and not a conclusion asserted in ZFC. -/ 51theorem hasDensityCharacter_atomicCounterexampleAlgebra_of_continuum_eq_aleph_one 52 (hCH : (Cardinal.continuum : Cardinal.{0}) = Cardinal.aleph 1) : 53 HasDensityCharacter AtomicCounterexampleAlgebra (Cardinal.aleph 1) := by 54 rw [← hCH] 55 exact hasDensityCharacter_atomicCounterexampleAlgebra 56 57/-- Every dense subset of the fixed irreducible Hilbert model is at least 58continuum-sized. This is norm density, not algebraic Hamel dimension. -/ 59theorem continuum_le_cardinalMk_dense_atomicCounterexampleHilbert 60 (s : Set (MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert 61 completedRootPureState)) (hs : Dense s) : Cardinal.continuum ≤ #s := 62 Representation.continuum_le_cardinalMk_dense_space_of_singleton_of_not_finiteDimensional 63 (shellFamilyInclusion homogeneityShellFamily) 64 (isUniqueIrreducibleModel_shellFamilyInclusion.{0} homogeneityShellFamily).2 65 (not_finiteDimensional_shellFamilyTarget homogeneityShellFamily) s hs 66 67/-- The cyclic orbit bounds the exact norm density of the fixed irreducible 68Hilbert model from above; the general Rosenberg bound gives the reverse. -/ 69theorem hasDensityCharacter_atomicCounterexampleHilbert : 70 HasDensityCharacter 71 (MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState) 72 Cardinal.continuum := by 73 let H := MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState 74 let pi : Representation AtomicCounterexampleAlgebra H := 75 shellFamilyInclusion homogeneityShellFamily 76 have hirr : Representation.IsIrreducible pi := 77 isIrreducible_shellFamilyInclusion homogeneityShellFamily 78 letI : Nontrivial H := Representation.nontrivial_of_isNonzero pi hirr.1 79 obtain ⟨x, hx⟩ : ∃ x : H, x ≠ 0 := exists_ne 0 80 let s : Set H := Set.range (fun a : AtomicCounterexampleAlgebra => pi a x) 81 have hs : Dense s := Representation.denseRange_orbitMap_of_isIrreducible pi hirr hx 82 have hupper' : Cardinal.lift.{0} (#s) ≤ 83 Cardinal.lift.{0} (#AtomicCounterexampleAlgebra) := Cardinal.mk_range_le_lift 84 have hupper : #s ≤ Cardinal.continuum := by 85 simpa [cardinalMk_atomicCounterexampleAlgebra] using hupper' 86 refine ⟨⟨s, hs, le_antisymm hupper 87 (continuum_le_cardinalMk_dense_atomicCounterexampleHilbert s hs)⟩, 88 continuum_le_cardinalMk_dense_atomicCounterexampleHilbert⟩ 89 90/-- The faithful separable model is infinite-dimensional: otherwise its 91operator algebra, and hence the faithfully represented source, would be finite-dimensional. -/ 92theorem not_finiteDimensional_separableCounterexampleHilbertSpace : 93 ¬ FiniteDimensional ℂ SeparableCounterexampleHilbertSpace := by 94 intro hfinite 95 letI : FiniteDimensional ℂ SeparableCounterexampleHilbertSpace := hfinite 96 letI : FiniteDimensional ℂ 97 (SeparableCounterexampleHilbertSpace →L[ℂ] SeparableCounterexampleHilbertSpace) := 98 ContinuousLinearMap.finiteDimensional 99 exact (not_finiteDimensional_shellFamilyTarget homogeneityShellFamily) 100 (FiniteDimensional.of_injective 101 (LinearMapClass.linearMap separableCounterexampleRepresentation) 102 separableCounterexampleRepresentation_injective) 103 104end MathlibAnnex.CStarAlgebra.CAR