CyclicGeneratorSpan.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Dense word-vector spans for cyclic generated algebras

A closed word span is reducing for each generator and hence for the generated von Neumann algebra. Containing the cyclic vector makes it all of the represented Hilbert space.

theorem OAI.KadisonKastler.invariant_closed_linearCombination_range line 23

Source documentation

Invariance on a spanning family passes to its closed linear span.

theorem invariant_closed_linearCombination_range
    (v : I → H) (T : H →L[ℂ] H)
    (h : ∀ i, T (v i) ∈ LinearMap.range (Finsupp.linearCombination ℂ v)) :
    ∀ x ∈ (LinearMap.range (Finsupp.linearCombination ℂ v)).topologicalClosure,
      T x ∈ (LinearMap.range (Finsupp.linearCombination ℂ v)).topologicalClosure := by
…

theorem OAI.KadisonKastler.denseRange_linearCombination_of_cyclic_generators line 41

Source documentation

A cyclic representation generated by a star-stable family is already cyclic on any invariant word span containing its cyclic vector.

theorem denseRange_linearCombination_of_cyclic_generators
    (M : VonNeumannAlgebra H) (Ω : H) (g : J → H →L[ℂ] H) (v : I → H)
    (hM : M = generatedVonNeumannAlgebra (StarAlgebra.adjoin ℂ (Set.range g)))
    (hcyclic : DenseRange (algebraVectorMap M Ω))
    (hstar : ∀ j, ∃ k, g k = star (g j))
    (hΩ : Ω ∈ LinearMap.range (Finsupp.linearCombination ℂ v))
    (hinv : ∀ j i, g j (v i) ∈ LinearMap.range (Finsupp.linearCombination ℂ v)) :
    DenseRange (Finsupp.linearCombination ℂ v) := by
…

Mentions: OAI.KadisonKastler.generatedVonNeumannAlgebra, OAI.KadisonKastler.algebraVectorMap