ConstantFieldCocycle.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Correcting a nearby unitary family into an algebra-valued cocycle

def OAI.KadisonKastler.algebraConstantField line 21
Source documentation
Constant fields with values in the specified von Neumann algebra.
```
def algebraConstantField (N : VonNeumannAlgebra H) :
    Algebra N →⋆ₐ[ℂ] operatorFieldAlgebra (μ := μ) N :=
…
```
Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.operatorFieldAlgebra
theorem OAI.KadisonKastler.algebraConstantField_coe line 35
def OAI.KadisonKastler.constantAlgebraUnitaryFamily line 40
Source documentation
A family of algebra unitaries determines a family of constant unitary fields.
```
def constantAlgebraUnitaryFamily (V : G → unitary (Algebra N)) :
    unitary (G →ᵇ operatorFieldAlgebra (μ := μ) N) :=
…
```
Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.operatorFieldAlgebra
theorem OAI.KadisonKastler.constantAlgebraUnitaryFamily_coe line 47

theorem OAI.KadisonKastler.constantAlgebraUnitaryFamily_defect_le line 53

Source documentation

The constant-field cocycle error is bounded by the ordinary group error.

theorem constantAlgebraUnitaryFamily_defect_le
    (α : NonsingularAction G D μ) (V : G → unitary (Algebra N))
    {e : ℝ} (he : 0 ≤ e)
    (hV : ∀ g h, ‖(V g : H →L[ℂ] H) * V h - V (g * h)‖ ≤ e) :
    unitaryCocycleDefect (α.restrictedOperatorAction N)
      (constantAlgebraUnitaryFamily (μ := μ) V) ≤ e := by
…

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

theorem OAI.KadisonKastler.operatorFieldConst_representative_ae line 73
Source documentation
The canonical representative of a constant field has the expected value almost everywhere.
```
theorem operatorFieldConst_representative_ae (T : H →L[ℂ] H) :
    ∀ᵐ x ∂μ, WeakOperatorRepresentative.eval
      (WeakOperatorField.representative (operatorFieldConst μ T)) x = T := by
…
```
Mentions: OAI.KadisonKastler.WeakOperatorRepresentative.eval, OAI.KadisonKastler.WeakOperatorField.representative, OAI.KadisonKastler.operatorFieldConst
theorem OAI.KadisonKastler.ScalarBoundaryMean.exists_measurable_cocycle_near_representation line 85
Source documentation
Starting from an actual nearby unitary family, correction supplies a measurable N-valued cocycle with the explicit total approximation bound.
```
theorem exists_measurable_cocycle_near_representation
    {α : NonsingularAction G D μ} (m : ScalarBoundaryMean α)
    (hTom : PublishedFieldTomiyama (G := G) (H := H) (μ := μ))
…
```
Mentions: OAI.KadisonKastler.NonsingularAction, OAI.KadisonKastler.ScalarBoundaryMean, OAI.KadisonKastler.PublishedFieldTomiyama