MeasurableOperatorCocycle.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Measurable unitary cocycles from the quotient construction

theorem OAI.KadisonKastler.exists_measurable_operator_cocycle_with_lift line 23
Source documentation
A quotient-valued cocycle admits measurable, everywhere unitary values. The cocycle identities and norm bound hold almost everywhere.
```
theorem exists_measurable_operator_cocycle_with_lift
    (α : NonsingularAction G D μ)
    (V W : unitary (G →ᵇ WeakOperatorField (H := H) μ))
…
```
Mentions: OAI.KadisonKastler.NonsingularAction, OAI.KadisonKastler.WeakOperatorField
theorem OAI.KadisonKastler.exists_measurable_operator_cocycle line 75
Source documentation
A quotient-valued cocycle admits measurable, everywhere unitary values. The cocycle identities and norm bound hold almost everywhere.
```
theorem exists_measurable_operator_cocycle
    (α : NonsingularAction G D μ)
    (V W : unitary (G →ᵇ WeakOperatorField (H := H) μ))
…
```
Mentions: OAI.KadisonKastler.NonsingularAction, OAI.KadisonKastler.WeakOperatorField

theorem OAI.KadisonKastler.measurable_cocycle_invariant_conull line 96

Source documentation

Countability makes all cocycle laws and norm bounds simultaneous on one invariant conull set.

theorem measurable_cocycle_invariant_conull [Countable G]
    (α : NonsingularAction G D μ) (U : G → D → unitary (H →L[ℂ] H))
    (L : G → D → H →L[ℂ] H) {r : ℝ}
    (hcoc : ∀ g h, ∀ᵐ x ∂μ,
      (U g x : H →L[ℂ] H) * (U h (α.toPerm g⁻¹ x) : H →L[ℂ] H) =
        (U (g * h) x : H →L[ℂ] H))
    (hclose : ∀ g, ∀ᵐ x ∂μ, ‖(U g x : H →L[ℂ] H) - L g x‖ ≤ r) :
    ∃ S : Set D, (∀ᵐ x ∂μ, x ∈ S) ∧
      (∀ g x, x ∈ S → α.toPerm g x ∈ S) ∧
      (∀ x ∈ S, ∀ g h,
        (U g x : H →L[ℂ] H) * (U h (α.toPerm g⁻¹ x) : H →L[ℂ] H) =
          (U (g * h) x : H →L[ℂ] H)) ∧
…

Mentions: OAI.KadisonKastler.NonsingularAction

theorem OAI.KadisonKastler.ScalarBoundaryMean.exists_measurable_correction line 129
Source documentation
The actual measurable correction theorem from a scalar boundary mean and the precisely cited Tomiyama bimodularity input.
```
theorem exists_measurable_correction (m : ScalarBoundaryMean α)
    (hTom : PublishedFieldTomiyama (G := G) (H := H) (μ := μ))
…
```
Mentions: OAI.KadisonKastler.ScalarBoundaryMean, OAI.KadisonKastler.PublishedFieldTomiyama