MeasurableFieldBicommutant.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Reconstructing operators in a represented bicommutant

If scalar localizations belong to a represented von Neumann algebra, every operator in its commutant has an actual measurable field. The fiber commutant theorem then shows that a bounded measurable field in the fiber bicommutants reconstructs an operator in the original bicommutant.

theorem OAI.KadisonSimilarity.boundedFieldOperator_mem_representationVonNeumannAlgebra line 27

Source documentation

A bounded measurable field in the genuine fiber bicommutants gives an operator in the global bicommutant. The localization hypothesis is ordinary membership of the scalar multiplication projections.

theorem boundedFieldOperator_mem_representationVonNeumannAlgebra
    (σ : A →⋆ₐ[ℂ] (Lp H 2 μ →L[ℂ] Lp H 2 μ))
    (ρ : ∀ _a : Ω, A →⋆ₐ[ℂ] (H →L[ℂ] H))
    (hσ : ∀ b : A, ∀ f : Lp H 2 μ,
      ∀ᵐ a ∂μ, σ b f a = ρ a b (f a))
    (hlocal : ∀ (s : Set Ω) (hs : MeasurableSet s),
      l2Localization μ s hs ∈ representationVonNeumannAlgebra σ)
    (Q : Ω → H →L[ℂ] H)
    (hmeas : ∀ x : H, AEStronglyMeasurable (fun a => Q a x) μ)
    (C : ℝ) (hbound : ∀ᵐ a ∂μ, ‖Q a‖ ≤ C)
    (hmem : ∀ᵐ a ∂μ, Q a ∈ representationVonNeumannAlgebra (ρ a)) :
    boundedFieldOperator μ Q hmeas C hbound ∈ representationVonNeumannAlgebra σ := by
…

Mentions: OAI.KadisonSimilarity.l2Localization, OAI.KadisonSimilarity.representationVonNeumannAlgebra, OAI.KadisonSimilarity.boundedFieldOperator

theorem OAI.KadisonSimilarity.boundedFieldOperator_mem_of_restricted_fiber_bicommutants line 59

Source documentation

The reconstruction needs genuine representations only on a measurable conull base. A global field can have any values on its null complement.

theorem boundedFieldOperator_mem_of_restricted_fiber_bicommutants
    (s : Set Ω) (hs : MeasurableSet s) (hnull : μ sᶜ = 0)
    (σ : A →⋆ₐ[ℂ] (Lp H 2 μ →L[ℂ] Lp H 2 μ))
    (ρ : ∀ _a : s, A →⋆ₐ[ℂ] (H →L[ℂ] H))
    (hσ : ∀ b : A, ∀ f : Lp H 2 μ,
      ∀ᵐ a : s ∂Measure.comap ((↑) : s → Ω) μ, σ b f a = ρ a b (f a))
    (hlocal : ∀ (t : Set Ω) (ht : MeasurableSet t),
      l2Localization μ t ht ∈ representationVonNeumannAlgebra σ)
    (Q : Ω → H →L[ℂ] H)
    (hmeas : ∀ x : H, AEStronglyMeasurable (fun a => Q a x) μ)
    (C : ℝ) (hbound : ∀ᵐ a ∂μ, ‖Q a‖ ≤ C)
    (hmem : ∀ᵐ a : s ∂Measure.comap ((↑) : s → Ω) μ,
…

Mentions: OAI.KadisonSimilarity.l2Localization, OAI.KadisonSimilarity.representationVonNeumannAlgebra

theorem OAI.KadisonSimilarity.boundedFieldOperator_central_of_restricted_fibers line 101

Source documentation

A bounded measurable central selector on the genuine conull fibers reconstructs a central operator in the represented von Neumann algebra.

theorem boundedFieldOperator_central_of_restricted_fibers
    (s : Set Ω) (hs : MeasurableSet s) (hnull : μ sᶜ = 0)
    (σ : A →⋆ₐ[ℂ] (Lp H 2 μ →L[ℂ] Lp H 2 μ))
    (ρ : ∀ _a : s, A →⋆ₐ[ℂ] (H →L[ℂ] H))
    (hσ : ∀ b : A, ∀ f : Lp H 2 μ,
      ∀ᵐ a : s ∂Measure.comap ((↑) : s → Ω) μ, σ b f a = ρ a b (f a))
    (hlocal : ∀ (t : Set Ω) (ht : MeasurableSet t),
      l2Localization μ t ht ∈ representationVonNeumannAlgebra σ)
    (Q : Ω → H →L[ℂ] H)
    (hmeas : ∀ x : H, AEStronglyMeasurable (fun a => Q a x) μ)
    (C : ℝ) (hbound : ∀ᵐ a ∂μ, ‖Q a‖ ≤ C)
    (hmem : ∀ᵐ a : s ∂Measure.comap ((↑) : s → Ω) μ,
…

Mentions: OAI.KadisonSimilarity.l2Localization, OAI.KadisonSimilarity.representationVonNeumannAlgebra