SpatialAssociatorAlgebra.lean`

18 declarations, 0 contain sorry, 0 declared as axioms

Associativity of represented spatial von Neumann products

The canonical Hilbert tensor associator transports the actual spatial product algebras. The passage from algebraic generators to their von Neumann algebras uses the existing bounded Kaplansky approximation input.

theorem OAI.KadisonKastler.spatialLeft_tendsto_strong line 29

Source documentation

Bounded strong convergence is preserved by the first tensor leg.

theorem spatialLeft_tendsto_strong
    {ι : Type*} {l : Filter ι} (T : ι → H →L[ℂ] H) (a : H →L[ℂ] H)
    {C : ℝ} (hT : ∀ i, ‖T i‖ ≤ C)
    (ha : ∀ x, Tendsto (fun i => T i x) l (𝓝 (a x)))
    (z : SpatialHilbert H K) :
    Tendsto (fun i => spatialLeft (K := K) (T i) z) l
…

Mentions: OAI.KadisonKastler.spatialLeft

theorem OAI.KadisonKastler.spatialLeft_mem_generated_contraction line 75

theorem OAI.KadisonKastler.spatialLeft_mem_generated line 97

Source documentation

The first-leg representation preserves membership in generated von Neumann algebras.

theorem spatialLeft_mem_generated
    (hK : PublishedKaplanskyDensity.{u})
    (B : StarSubalgebra ℂ (H →L[ℂ] H))
    (A : StarSubalgebra ℂ (SpatialHilbert H K →L[ℂ] SpatialHilbert H K))
    (hBA : ∀ b ∈ B, spatialLeft (K := K) b ∈ A)
…

Mentions: OAI.KadisonKastler.spatialLeft

theorem OAI.KadisonKastler.generated_of_vonNeumann line 118
theorem OAI.KadisonKastler.spatialLeft_mem_of_generated line 124
theorem OAI.KadisonKastler.spatialRight_mem_of_generated line 133
theorem OAI.KadisonKastler.assoc_left_left line 151
theorem OAI.KadisonKastler.assoc_left_right line 160
theorem OAI.KadisonKastler.assoc_right line 166
theorem OAI.KadisonKastler.mem_assoc_pullback line 176
theorem OAI.KadisonKastler.assoc_forward_le line 185
theorem OAI.KadisonKastler.conj_mem_transport line 227
theorem OAI.KadisonKastler.assoc_left_mem line 235
theorem OAI.KadisonKastler.assoc_middle_mem line 246
theorem OAI.KadisonKastler.assoc_right_mem line 257
theorem OAI.KadisonKastler.assoc_inner_generators_mem line 267
theorem OAI.KadisonKastler.assoc_reverse_le line 285
theorem OAI.KadisonKastler.spatialTransport_spatialProduct_assoc line 298
Source documentation
The canonical tensor associator identifies the represented spatial products.
```
theorem spatialTransport_spatialProduct_assoc
    (hK : PublishedKaplanskyDensity.{u})
    (M : VonNeumannAlgebra H) (N : VonNeumannAlgebra K) (P : VonNeumannAlgebra L) :
    spatialTransportAlgebra (spatialAssociator (H := H) (K := K) (L := L))
…
```
Mentions: OAI.KadisonKastler.spatialTransportAlgebra, OAI.KadisonKastler.spatialAssociator