BoundaryErgodicReduction.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Removing the boundary variables by double ergodicity

The diagonal comparison gives the vector field L* a Ω. Its covariance is derived from the product intertwiner and the tracial right action. Double ergodicity is used only for this actual bounded measurable field.

theorem OAI.KadisonKastler.aestronglyMeasurable_field_apply line 30
Source documentation
Strongly measurable evaluations of an operator field can be applied to a varying strongly measurable vector. No operator-norm measurability of the field is required.
```
theorem aestronglyMeasurable_field_apply (T : P → H →L[ℂ] H)
    (hT : ∀ ξ, AEStronglyMeasurable (fun p => T p ξ) μ)
    (v : P → H) (hv : AEStronglyMeasurable v μ) :
    AEStronglyMeasurable (fun p => T p (v p)) μ := by
…
```

theorem OAI.KadisonKastler.boundary_intertwiner_adjoint line 58

Source documentation

The operator identity behind the equivariance of L* a Ω.

theorem boundary_intertwiner_adjoint (L K U V : unitary (H →L[ℂ] H))
    (h : (L : H →L[ℂ] H) * U = (V : H →L[ℂ] H) * K) :
    star (L : H →L[ℂ] H) * V = (U : H →L[ℂ] H) * star (K : H →L[ℂ] H) := by
…

theorem OAI.KadisonKastler.boundary_comparison_vector_covariance line 71

Source documentation

Diagonal covariance follows from the genuine right-action identities.

theorem boundary_comparison_vector_covariance
    (L K U W Z R a b : unitary (H →L[ℂ] H)) (Ω : H)
    (hL : (L : H →L[ℂ] H) * U = ((W : H →L[ℂ] H) * R) * K)
    (ha : (a : H →L[ℂ] H) = ((W : H →L[ℂ] H) * b) * star (Z : H →L[ℂ] H))
    (hR : (R : H →L[ℂ] H) * b = (b : H →L[ℂ] H) * R)
    (hΩ : (R : H →L[ℂ] H) Ω = star (Z : H →L[ℂ] H) Ω) :
    star (L : H →L[ℂ] H) ((a : H →L[ℂ] H) Ω) =
      (U : H →L[ℂ] H) (star (K : H →L[ℂ] H) ((b : H →L[ℂ] H) Ω)) := by
…

def OAI.KadisonKastler.scalarUnitaryOfNormOne line 92
Source documentation
The scalar phase supplied by the invariant vector defines a unitary scalar operator.
```
def scalarUnitaryOfNormOne (z : ℂ) (hz : ‖z‖ = 1) : unitary (H →L[ℂ] H) :=
…
```

theorem OAI.KadisonKastler.normalized_boundary_unitary_fixes line 103

Source documentation

A constant unit vector of the form L* a Ω = z Ω gives the normalized unitary z a* L fixing Ω.

theorem normalized_boundary_unitary_fixes
    (L a : unitary (H →L[ℂ] H)) (Ω : H) (z : ℂ) (hz : ‖z‖ = 1)
    (hv : star (L : H →L[ℂ] H) ((a : H →L[ℂ] H) Ω) = z • Ω) :
    ((scalarUnitaryOfNormOne z hz * star a * L : unitary (H →L[ℂ] H)) :
      H →L[ℂ] H) Ω = Ω := by
…

Mentions: OAI.KadisonKastler.scalarUnitaryOfNormOne

theorem OAI.KadisonKastler.normalized_boundary_unitary_distance line 116

theorem OAI.KadisonKastler.normalized_boundary_unitary_image line 142

Source documentation

The one-sided product intertwiner gives the precise unitary image of each group vector after scalar normalization.

theorem normalized_boundary_unitary_image
    (L K a b U W : unitary (H →L[ℂ] H)) (Ω : H) (z : ℂ)
    (hL : (L : H →L[ℂ] H) * U = (W : H →L[ℂ] H) * K)
    (hK : star (K : H →L[ℂ] H) ((b : H →L[ℂ] H) Ω) = z • Ω) :
    (z • (star (a : H →L[ℂ] H) * L)) ((U : H →L[ℂ] H) Ω) =
      (star (a : H →L[ℂ] H) * W * b) Ω := by
…

theorem OAI.KadisonKastler.boundary_unitary_image_distance line 162

Source documentation

The image unitaries stay close to the original group elements.

theorem boundary_unitary_image_distance (a b W U : unitary (H →L[ℂ] H)) :
    ‖star (a : H →L[ℂ] H) * W * b - U‖ ≤
      ‖(a : H →L[ℂ] H) - 1‖ + ‖(W : H →L[ℂ] H) - U‖ +
        ‖(b : H →L[ℂ] H) - 1‖ := by
…

theorem OAI.KadisonKastler.exists_boundary_scalar_of_doubleErgodic line 204

Source documentation

Applying genuine double ergodicity to the diagonal comparison field produces its scalar phase and the quantitative near-one bound.

theorem exists_boundary_scalar_of_doubleErgodic
    (α : NonsingularAction G D μ) (herg : UnitaryDoubleErgodic.{uG, uD, uH} α)
    (σ : G →* unitary (H →L[ℂ] H)) (Ω : H) (hΩ : ‖Ω‖ = 1)
    (hfixed : ∀ v : H, (∀ g, (σ g : H →L[ℂ] H) v = v) → ∃ z : ℂ, v = z • Ω)
    (L a : D × D → unitary (H →L[ℂ] H))
    (hLm : ∀ ξ, AEStronglyMeasurable
      (fun p => star (L p : H →L[ℂ] H) ξ) (μ.prod μ))
    (ham : AEStronglyMeasurable (fun p => (a p : H →L[ℂ] H) Ω) (μ.prod μ))
    (hcov : ∀ g, ∀ᵐ p ∂μ.prod μ,
      star (L (α.diagonal.toPerm g p) : H →L[ℂ] H)
        ((a (α.diagonal.toPerm g p) : H →L[ℂ] H) Ω) =
      (σ g : H →L[ℂ] H) (star (L p : H →L[ℂ] H) ((a p : H →L[ℂ] H) Ω)))
…

Mentions: OAI.KadisonKastler.NonsingularAction

theorem OAI.KadisonKastler.exists_boundary_scalar_from_comparison line 249

Source documentation

The field used in double ergodicity is equivariant as a consequence of the product intertwiner, diagonal comparison and tracial right action.

theorem exists_boundary_scalar_from_comparison
    (α : NonsingularAction G D μ) (herg : UnitaryDoubleErgodic.{uG, uD, uH} α)
    (σ : G →* unitary (H →L[ℂ] H)) (Ω : H) (hΩ : ‖Ω‖ = 1)
    (hfixed : ∀ v : H, (∀ g, (σ g : H →L[ℂ] H) v = v) → ∃ z : ℂ, v = z • Ω)
    (L a : D × D → unitary (H →L[ℂ] H))
    (W R : G → D → unitary (H →L[ℂ] H))
    (hLm : ∀ ξ, AEStronglyMeasurable
      (fun p => star (L p : H →L[ℂ] H) ξ) (μ.prod μ))
    (ham : AEStronglyMeasurable (fun p => (a p : H →L[ℂ] H) Ω) (μ.prod μ))
    (hL : ∀ g, ∀ᵐ p ∂μ.prod μ,
      (L p : H →L[ℂ] H) * σ g =
        ((W g p.1 : H →L[ℂ] H) * R g p.2) * L (α.diagonal.toPerm g⁻¹ p))
…

Mentions: OAI.KadisonKastler.NonsingularAction

theorem OAI.KadisonKastler.exists_simultaneous_boundary_normalization line 293

Source documentation

Choose one pair on which the scalar-vector relation and all group intertwiners hold simultaneously, including their separate translates.

theorem exists_simultaneous_boundary_normalization [Countable G]
    (α : NonsingularAction G D μ) (Ω : H)
    (L a : D × D → unitary (H →L[ℂ] H))
    (U : G → unitary (H →L[ℂ] H)) (W : G → D → unitary (H →L[ℂ] H))
    (z : ℂ) (hz : ‖z‖ = 1)
    (hvec : ∀ᵐ p ∂μ.prod μ,
      star (L p : H →L[ℂ] H) ((a p : H →L[ℂ] H) Ω) = z • Ω)
    (hL : ∀ g, ∀ᵐ p ∂μ.prod μ,
      (L p : H →L[ℂ] H) * U g = (W g p.1 : H →L[ℂ] H) *
        L (α.toPerm g⁻¹ p.1, p.2))
    {εL εa εW : ℝ} (hznear : ‖z - 1‖ ≤ εL + εa)
    (hLn : ∀ᵐ p ∂μ.prod μ, ‖(L p : H →L[ℂ] H) - 1‖ ≤ εL)
…

Mentions: OAI.KadisonKastler.NonsingularAction