ProjectionCentralData.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Central-decomposition data from actual projection fields

The construction uses the original measure space. On the null complement of the genuine unitized representations, the original algebra acts by zero and its unit range is the zero Hilbert space. Algebraic laws, norm formulas, von Neumann membership and countable contraction tests are all derived from the actual L² action identities.

abbrev OAI.KadisonSimilarity.conullProjectionFiber line 31
Source documentation
The genuine old-unit range at every base point, including zero fibers on the null complement of the original representations.
```
abbrev conullProjectionFiber {A : Type u} [CStarAlgebra A]
    (s : Set Ω) (ρ : ∀ _x : s, Unitization ℂ A →⋆ₐ[ℂ] (F →L[ℂ] F)) (x : Ω) : Type u :=
…
```
theorem OAI.KadisonSimilarity.conull_projection_membership line 37
theorem OAI.KadisonSimilarity.fields_eq_of_same_action line 64
theorem OAI.KadisonSimilarity.isometric_raw_field_sub line 75
theorem OAI.KadisonSimilarity.isometric_raw_field_mul line 94

theorem OAI.KadisonSimilarity.ae_global_projection_mem_of_isometric_closure line 112

Source documentation

A represented bicommutant member has its actual global field in the bicommutant of the old-unit range representation almost everywhere. This transports the conull membership statement without choosing arbitrary representations on the null complement.

theorem ae_global_projection_mem_of_isometric_closure
    {A : Type u} [CStarAlgebra A]
    (s : Set Ω) (hs : MeasurableSet s) (hnull : μ sᶜ = 0)
    (J : H →ₗᵢ[ℂ] Lp F 2 μ) (σ : A →⋆ₐ[ℂ] (H →L[ℂ] H))
    (ρ : ∀ _x : s, Unitization ℂ A →⋆ₐ[ℂ] (F →L[ℂ] F))
    (hρ : ∀ a : A, ∀ f : Lp F 2 μ,
      ∀ᵐ x : s ∂Measure.comap ((↑) : s → Ω) μ,
        isometricExtension J (σ a) f x = ρ x (Unitization.inr a) (f x))
    (T : H →L[ℂ] H) (hT : T ∈ representationVonNeumannAlgebra σ)
    (R : Ω → F →L[ℂ] F)
    (hR : ∀ f : Lp F 2 μ, ∀ᵐ x ∂μ, isometricExtension J T f x = R x (f x)) :
    ∀ᵐ x ∂μ, projectionFiberCompression
…

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

def OAI.KadisonSimilarity.projectionCentralData line 149

Source documentation

Construct all the direct-integral data needed for the separable commutator estimate, before the separate factor-fiber theorem. The only geometric inputs are genuine conull representations and actual L² action identities for the isometric extension.

def projectionCentralData
    (P : VonNeumannAlgebra H)
    (B : StarSubalgebra ℂ (H →L[ℂ] H)) [IsClosed (B : Set (H →L[ℂ] H))]
    [TopologicalSpace.SeparableSpace B]
    (hB : B ≤ P.toStarSubalgebra)
    (hgen : representationVonNeumannAlgebra B.subtype = P)
    (s : Set Ω) (hs : MeasurableSet s) (hnull : μ sᶜ = 0)
    (J : H →ₗᵢ[ℂ] Lp F 2 μ)
    (ρ : ∀ _x : s, Unitization ℂ B →⋆ₐ[ℂ] (F →L[ℂ] F))
    (hρ : ∀ b : B, ∀ f : Lp F 2 μ,
      ∀ᵐ x : s ∂Measure.comap ((↑) : s → Ω) μ,
        isometricExtension J (b : H →L[ℂ] H) f x = ρ x (Unitization.inr b) (f x))
…

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