MeasurableProductCocycle.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

The product cocycle as a measurable operator class

The pointwise two-sided field is measurable and uniformly unitary. Its class satisfies the separate-action cocycle law even when the original cocycle and algebra-membership statements hold only almost everywhere.

theorem OAI.KadisonKastler.productBoundaryValue_aestronglyMeasurable line 29

Source documentation

Evaluation of the product field is strongly measurable.

theorem productBoundaryValue_aestronglyMeasurable {N : VonNeumannAlgebra H}
    (p : StandardTracialPosition N) (W : G → D → unitary (H →L[ℂ] H))
    (hW : ∀ g ξ, AEStronglyMeasurable (fun x => (W g x : H →L[ℂ] H) ξ) μ)
    (g : G × G) (ξ : H) :
    AEStronglyMeasurable
      (fun x : D × D => (productBoundaryValue p W g x : H →L[ℂ] H) ξ) (μ.prod μ) := by
…

Mentions: OAI.KadisonKastler.StandardTracialPosition, OAI.KadisonKastler.productBoundaryValue

def OAI.KadisonKastler.measurableUnitaryRepresentative line 47

Source documentation

Bundle an everywhere unitary field from measurable evaluations.

def measurableUnitaryRepresentative {X : Type*} [MeasurableSpace X] {ν : Measure X}
    (f : X → unitary (H →L[ℂ] H))
    (hf : ∀ ξ, AEStronglyMeasurable (fun x => (f x : H →L[ℂ] H) ξ) ν) :
    unitary (WeakOperatorRepresentative (H := H) ν) := by
…

Mentions: OAI.KadisonKastler.WeakOperatorRepresentative

def OAI.KadisonKastler.productBoundaryRepresentative line 66

Source documentation

A uniformly unitary representative of the product field.

def productBoundaryRepresentative {N : VonNeumannAlgebra H}
    (p : StandardTracialPosition N) (W : G → D → unitary (H →L[ℂ] H))
    (hW : ∀ g ξ, AEStronglyMeasurable (fun x => (W g x : H →L[ℂ] H) ξ) μ)
    (g : G × G) : unitary (WeakOperatorRepresentative (H := H) (μ.prod μ)) :=
…

Mentions: OAI.KadisonKastler.StandardTracialPosition, OAI.KadisonKastler.WeakOperatorRepresentative

theorem OAI.KadisonKastler.productBoundaryRepresentative_eval line 75

def OAI.KadisonKastler.productBoundaryClass line 84

Source documentation

The actual bounded family of unitary classes on the product boundary.

def productBoundaryClass {N : VonNeumannAlgebra H}
    (p : StandardTracialPosition N) (W : G → D → unitary (H →L[ℂ] H))
    (hW : ∀ g ξ, AEStronglyMeasurable (fun x => (W g x : H →L[ℂ] H) ξ) μ) :
    unitary ((G × G) →ᵇ WeakOperatorField (H := H) (μ.prod μ)) :=
…

Mentions: OAI.KadisonKastler.StandardTracialPosition, OAI.KadisonKastler.WeakOperatorField

theorem OAI.KadisonKastler.productBoundaryClass_apply line 93

theorem OAI.KadisonKastler.productBoundaryClass_cocycle line 101

Source documentation

The product cocycle law descends from almost-everywhere original laws.

theorem productBoundaryClass_cocycle {N : VonNeumannAlgebra H}
    (p : StandardTracialPosition N) (α : NonsingularAction G D μ)
    (W : G → D → unitary (H →L[ℂ] H))
    (hW : ∀ g ξ, AEStronglyMeasurable (fun x => (W g x : H →L[ℂ] H) ξ) μ)
    (hmem : ∀ g, ∀ᵐ x ∂μ, (W g x : H →L[ℂ] H) ∈ N)
    (hcoc : ∀ g h, ∀ᵐ x ∂μ,
      (W g x : H →L[ℂ] H) * (W h (α.toPerm g⁻¹ x) : H →L[ℂ] H) =
        (W (g * h) x : H →L[ℂ] H)) (g h : G × G) :
    (productBoundaryClass p W hW).val g *
        α.prod.operatorAction (H := H) g ((productBoundaryClass p W hW).val h) =
…

Mentions: OAI.KadisonKastler.StandardTracialPosition, OAI.KadisonKastler.NonsingularAction, OAI.KadisonKastler.productBoundaryClass

def OAI.KadisonKastler.productBoundaryConstantFamily line 137
Source documentation
The corresponding representation as a family of constant operator classes.
```
def productBoundaryConstantFamily {M : VonNeumannAlgebra H}
    (p : StandardTracialPosition M) (U : G →* unitary (Algebra M)) :
    unitary ((G × G) →ᵇ WeakOperatorField (H := H) (μ.prod μ)) :=
…
```
Mentions: OAI.KadisonKastler.StandardTracialPosition, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.WeakOperatorField

theorem OAI.KadisonKastler.productBoundaryValue_close_at line 146

Source documentation

The two individual approximation inequalities suffice for the product bound.

theorem productBoundaryValue_close_at {M N : VonNeumannAlgebra H}
    (pM : StandardTracialPosition M) (pN : StandardTracialPosition N)
    (U : G →* unitary (Algebra M)) (W : G → D → unitary (H →L[ℂ] H))
    {δ κ : ℝ} (hδ : 0 ≤ δ) (hκ : 0 ≤ κ)
    (hJ : ‖(pM.conjugation : H →L⋆[ℂ] H) - (pN.conjugation : H →L⋆[ℂ] H)‖ ≤ κ)
    (g : G × G) (x : D × D)
    (hl : ‖(W g.1 x.1 : H →L[ℂ] H) - (U g.1 : Algebra M).val‖ ≤ δ)
    (hr : ‖(W g.2 x.2 : H →L[ℂ] H) - (U g.2 : Algebra M).val‖ ≤ δ) :
    ‖(productBoundaryValue pN W g x : H →L[ℂ] H) -
      (productBoundaryRepresentation pM U g : H →L[ℂ] H)‖ ≤ 2 * δ + 2 * κ := by
…

Mentions: OAI.KadisonKastler.StandardTracialPosition, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.productBoundaryValue, OAI.KadisonKastler.productBoundaryRepresentation

theorem OAI.KadisonKastler.productBoundaryClass_close line 163

Source documentation

Essential original closeness bounds the uniform norm of the product classes.

theorem productBoundaryClass_close {M N : VonNeumannAlgebra H}
    (pM : StandardTracialPosition M) (pN : StandardTracialPosition N)
    (U : G →* unitary (Algebra M)) (W : G → D → unitary (H →L[ℂ] H))
    (hW : ∀ g ξ, AEStronglyMeasurable (fun x => (W g x : H →L[ℂ] H) ξ) μ)
    {δ κ : ℝ} (hδ : 0 ≤ δ) (hκ : 0 ≤ κ)
    (hclose : ∀ g, ∀ᵐ x ∂μ, ‖(W g x : H →L[ℂ] H) - (U g : Algebra M).val‖ ≤ δ)
    (hJ : ‖(pM.conjugation : H →L⋆[ℂ] H) - (pN.conjugation : H →L⋆[ℂ] H)‖ ≤ κ) :
    ‖(productBoundaryClass pN W hW).val - (productBoundaryConstantFamily (μ := μ) pM U).val‖ ≤
…

Mentions: OAI.KadisonKastler.StandardTracialPosition, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.productBoundaryClass, OAI.KadisonKastler.productBoundaryConstantFamily