ProjectionFieldClosure.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Closure in the genuine projection-fiber algebras

Strong Kaplansky approximation first proves membership in the raw unitized fiber algebra. Compression to the old-unit range then gives membership in the genuine representation of the original algebra. No representation on the null complement is needed.

theorem OAI.KadisonSimilarity.ae_unitization_field_mem_of_isometric_closure line 29

Source documentation

The conull raw unitized fiber representations contain the field of every operator in the original represented bicommutant.

theorem ae_unitization_field_mem_of_isometric_closure
    (s : Set Ω) (hs : MeasurableSet s) (hnull : μ sᶜ = 0)
    (J : H →ₗᵢ[ℂ] Lp F 2 μ) (σ : B →⋆ₐ[ℂ] (H →L[ℂ] H))
    (ρ : ∀ _x : s, Unitization ℂ B →⋆ₐ[ℂ] (F →L[ℂ] F))
    (hρ : ∀ b : B, ∀ f : Lp F 2 μ,
      ∀ᵐ x : s ∂Measure.comap ((↑) : s → Ω) μ,
        isometricExtension J (σ b) f x = ρ x (Unitization.inr b) (f x))
    (T : H →L[ℂ] H) (hT : T ∈ representationVonNeumannAlgebra σ)
    (Q : s → F →L[ℂ] F)
    (hQ : ∀ f : Lp F 2 μ,
      ∀ᵐ x : s ∂Measure.comap ((↑) : s → Ω) μ,
        isometricExtension J T f x = Q x (f x)) :
…

Mentions: OAI.KadisonSimilarity.isometricExtension, OAI.KadisonSimilarity.representationVonNeumannAlgebra

theorem OAI.KadisonSimilarity.ae_projection_field_mem_of_isometric_closure line 70

Source documentation

Passing to the old-unit range yields membership in the actual variable-fiber representation of the original algebra.

theorem ae_projection_field_mem_of_isometric_closure
    (s : Set Ω) (hs : MeasurableSet s) (hnull : μ sᶜ = 0)
    (J : H →ₗᵢ[ℂ] Lp F 2 μ) (σ : B →⋆ₐ[ℂ] (H →L[ℂ] H))
    (ρ : ∀ _x : s, Unitization ℂ B →⋆ₐ[ℂ] (F →L[ℂ] F))
    (hρ : ∀ b : B, ∀ f : Lp F 2 μ,
      ∀ᵐ x : s ∂Measure.comap ((↑) : s → Ω) μ,
        isometricExtension J (σ b) f x = ρ x (Unitization.inr b) (f x))
    (T : H →L[ℂ] H) (hT : T ∈ representationVonNeumannAlgebra σ)
    (Q : s → F →L[ℂ] F)
    (hQ : ∀ f : Lp F 2 μ,
      ∀ᵐ x : s ∂Measure.comap ((↑) : s → Ω) μ,
        isometricExtension J T f x = Q x (f x)) :
…

Mentions: OAI.KadisonSimilarity.isometricExtension, OAI.KadisonSimilarity.representationVonNeumannAlgebra