RegularCoreIntersection.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The joint fixed algebra in the concrete regular representation

The reverse tensor membership is proved from the actual multiplier representation. The joint fixed-point identification then uses only the two separate published spectral and diagonal decomposition inputs.

theorem OAI.KadisonKastler.continuous_unitary_field_apply line 29

Source documentation

Strong continuity of a unitary field permits a continuously varying vector argument, because every member is an isometry.

theorem continuous_unitary_field_apply {X : Type*} [TopologicalSpace X]
    (V : X → unitary (H →L[ℂ] H))
    (hV : ∀ ξ, Continuous (fun x => (V x : H →L[ℂ] H) ξ))
    (f : X → H) (hf : Continuous f) :
    Continuous (fun x => (V x : H →L[ℂ] H) (f x)) := by
…

theorem OAI.KadisonKastler.regularCoreEmbedding_field_continuous line 56
theorem OAI.KadisonKastler.regularCoreEmbedding_mem_tensorAlgebra_iff line 76
Source documentation
Membership in the tensor algebra reflects membership in the original algebra. The coefficient identity is continuous, so its almost-everywhere validity also gives its value at zero.
```
theorem regularCoreEmbedding_mem_tensorAlgebra_iff (P : VonNeumannAlgebra H)
    (hP : ∀ s A, A ∈ P → unitaryConj (U s) A ∈ P) (A : H →L[ℂ] H) :
    regularCoreEmbedding U hU A ∈ regularTensorAlgebra P ↔ A ∈ P := by
…
```
Mentions: OAI.KadisonKastler.unitaryConj, OAI.KadisonKastler.regularCoreEmbedding, OAI.KadisonKastler.regularTensorAlgebra
theorem OAI.KadisonKastler.mem_regular_jointFixed_iff line 118
Source documentation
The exact joint fixed algebra of the two concrete regular actions. The spectral and diagonal decomposition inputs are used separately; the algebra identification itself is the conclusion of the proof.
```
theorem mem_regular_jointFixed_iff [TopologicalSpace.SeparableSpace H]
    (hSpectral : PublishedRealSpectralCommutant.{u})
    (hDiagonal : PublishedRealDiagonalDecomposition.{u})
    (P : VonNeumannAlgebra H)
    (hP : ∀ s A, A ∈ P → unitaryConj (U s) A ∈ P)
    (T : RegularCoreHilbert H →L[ℂ] RegularCoreHilbert H) :
    T ∈ fixedPointAlgebra (regularCharacterRepresentation (H := H))
…
```
Mentions: OAI.KadisonKastler.unitaryConj, OAI.KadisonKastler.RegularCoreHilbert, OAI.KadisonKastler.fixedPointAlgebra, OAI.KadisonKastler.regularCharacterRepresentation