AlgebraCocycleRepresentatives.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Algebra-valued representatives of an almost-everywhere cocycle

An ambient unitary lying in a von Neumann algebra is a unitary of that algebra. Replacing exceptional values by one therefore makes the entire family algebra-valued without changing any measurable or cocycle data.

def OAI.KadisonKastler.unitaryInAlgebra line 21
Source documentation
Regard an ambient unitary contained in an algebra as a unitary of it.
```
def unitaryInAlgebra (M : VonNeumannAlgebra H) (u : unitary (H →L[ℂ] H))
    (hu : (u : H →L[ℂ] H) ∈ M) : unitary (Algebra M) :=
…
```
Mentions: OAI.KadisonKastler.Algebra
theorem OAI.KadisonKastler.unitaryInAlgebra_coe line 31
def OAI.KadisonKastler.algebraCocycleRepresentative line 38
Source documentation
Replace the exceptional values of an ambient unitary family by one.
```
def algebraCocycleRepresentative (M : VonNeumannAlgebra H)
    (W : G → D → unitary (H →L[ℂ] H)) (g : G) (x : D) : unitary (Algebra M) := by
…
```
Mentions: OAI.KadisonKastler.Algebra
theorem OAI.KadisonKastler.algebraCocycleRepresentative_ae line 45

theorem OAI.KadisonKastler.algebraCocycleRepresentative_measurable line 54

Source documentation

Measurable evaluations survive the exceptional-set replacement.

theorem algebraCocycleRepresentative_measurable (M : VonNeumannAlgebra H)
    (W : G → D → unitary (H →L[ℂ] H))
    (hmem : ∀ g, ∀ᵐ x ∂μ, (W g x : H →L[ℂ] H) ∈ M)
    (hmeas : ∀ g ξ, AEStronglyMeasurable (fun x => (W g x : H →L[ℂ] H) ξ) μ)
    (g : G) (ξ : H) :
    AEStronglyMeasurable
      (fun x => (algebraCocycleRepresentative M W g x : Algebra M).val ξ) μ :=
…

Mentions: OAI.KadisonKastler.algebraCocycleRepresentative, OAI.KadisonKastler.Algebra

theorem OAI.KadisonKastler.algebraCocycleRepresentative_cocycle line 68

Source documentation

Nonsingularity transports the exceptional null set in the second factor of the cocycle identity.

theorem algebraCocycleRepresentative_cocycle (M : VonNeumannAlgebra H)
    (α : NonsingularAction G D μ) (W : G → D → unitary (H →L[ℂ] H))
    (hmem : ∀ g, ∀ᵐ x ∂μ, (W g x : H →L[ℂ] H) ∈ M)
    (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) :
    ∀ᵐ x ∂μ,
      (algebraCocycleRepresentative M W g x : Algebra M) *
        (algebraCocycleRepresentative M W h (α.toPerm g⁻¹ x) : Algebra M) =
          (algebraCocycleRepresentative M W (g * h) x : Algebra M) := by
…

Mentions: OAI.KadisonKastler.NonsingularAction, OAI.KadisonKastler.algebraCocycleRepresentative, OAI.KadisonKastler.Algebra

theorem OAI.KadisonKastler.algebraCocycleRepresentative_close line 90

Source documentation

Any essential closeness estimate is retained with the same constant.

theorem algebraCocycleRepresentative_close (M : VonNeumannAlgebra H)
    (W : G → D → unitary (H →L[ℂ] H))
    (hmem : ∀ g, ∀ᵐ x ∂μ, (W g x : H →L[ℂ] H) ∈ M)
    (U : G → H →L[ℂ] H) {δ : ℝ}
    (hclose : ∀ g, ∀ᵐ x ∂μ, ‖(W g x : H →L[ℂ] H) - U g‖ ≤ δ) (g : G) :
    ∀ᵐ x ∂μ, ‖(algebraCocycleRepresentative M W g x : Algebra M).val - U g‖ ≤ δ := by
…

Mentions: OAI.KadisonKastler.algebraCocycleRepresentative, OAI.KadisonKastler.Algebra

theorem OAI.KadisonKastler.exists_algebra_cocycle_representatives line 100

Source documentation

A typed algebra-valued cocycle, with all the original measurable data.

theorem exists_algebra_cocycle_representatives (M : VonNeumannAlgebra H)
    (α : NonsingularAction G D μ) (W : G → D → unitary (H →L[ℂ] H))
    (hmem : ∀ g, ∀ᵐ x ∂μ, (W g x : H →L[ℂ] H) ∈ M)
    (hmeas : ∀ g ξ, AEStronglyMeasurable (fun x => (W g x : H →L[ℂ] H) ξ) μ)
    (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)) :
    ∃ WN : G → D → unitary (Algebra M),
      (∀ g, ∀ᵐ x ∂μ, (WN g x : Algebra M).val = (W g x : H →L[ℂ] H)) ∧
      (∀ g ξ, AEStronglyMeasurable (fun x => (WN g x : Algebra M).val ξ) μ) ∧
      (∀ g h, ∀ᵐ x ∂μ, (WN g x : Algebra M) *
        (WN h (α.toPerm g⁻¹ x) : Algebra M) = (WN (g * h) x : Algebra M)) := by
…

Mentions: OAI.KadisonKastler.NonsingularAction, OAI.KadisonKastler.Algebra