AEBoundaryDiagonal.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Diagonal comparison from almost-everywhere cocycle data

A countable group has a common invariant conull set for the cocycle laws and approximation bounds. Outside that set the generating family is filled with one good value. This provides global bounds for the least-vector and polar constructions; covariance is required only on the conull set.

theorem OAI.KadisonKastler.exists_measurable_diagonal_unitary_on_set line 35

Source documentation

Global boundedness suffices for the measurable least field. The cocycle laws need hold only on the set where covariance is asserted.

theorem exists_measurable_diagonal_unitary_on_set
    (J : Algebra M →ₗ[ℂ] E) (hJ : ∀ x, ‖J x‖ = traceTwoNorm τ x)
    (hτ : FiniteVectorTrace τ)
    {G D : Type*} [Group G] [Countable G] [MeasurableSpace D] {μ : Measure (D × D)}
    (S : Set D) (shift : G → D → D) (W : G → D → unitary (Algebra M))
    (hW : ∀ g t x, x ∈ S → (W (g * t) x : Algebra M) =
      (W g x : Algebra M) * (W t (shift g x) : Algebra M))
    (hWmeas : ∀ t, AEStronglyMeasurable
      (fun p : D × D => J ((W t p.1 : Algebra M) * star (W t p.2 : Algebra M))) μ)
    {r : ℝ} (hr0 : 0 ≤ r) (hr : r < 1)
    (hnear : ∀ t x y, ‖(W t x : Algebra M) * star (W t y : Algebra M) - 1‖ ≤ r) :
    ∃ a : D → D → unitary (Algebra M),
…

Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.traceTwoNorm, OAI.KadisonKastler.FiniteVectorTrace

theorem OAI.KadisonKastler.norm_unitary_mul_star_sub_one line 125
Source documentation
The unitary-pair displacement equals the distance between the pair.
```
theorem norm_unitary_mul_star_sub_one (u v : unitary (Algebra M)) :
    ‖(u : Algebra M) * star (v : Algebra M) - 1‖ = ‖(u : Algebra M) - v‖ := by
…
```
Mentions: OAI.KadisonKastler.Algebra

theorem OAI.KadisonKastler.exists_ae_measurable_diagonal_unitary_comparison line 135

Source documentation

Countably many almost-everywhere laws give the diagonal comparison, with its explicit 4δ displacement and almost-everywhere covariance.

theorem exists_ae_measurable_diagonal_unitary_comparison
    (J : Algebra M →ₗ[ℂ] E) (hJ : ∀ x, ‖J x‖ = traceTwoNorm τ x)
    (hτ : FiniteVectorTrace τ) (α : NonsingularAction G D μ)
    (W : G → D → unitary (Algebra M))
    (hW : ∀ g t, ∀ᵐ x ∂μ, (W (g * t) x : Algebra M) =
      (W g x : Algebra M) * (W t (α.toPerm g⁻¹ x) : Algebra M))
    (hWmeas : ∀ t, AEStronglyMeasurable
      (fun p : D × D => J ((W t p.1 : Algebra M) * star (W t p.2 : Algebra M))) (μ.prod μ))
    (U : G → unitary (H →L[ℂ] H)) {δ : ℝ} (hδ : 0 ≤ δ) (hsmall : 2 * δ < 1)
    (hclose : ∀ g, ∀ᵐ x ∂μ, ‖(W g x : Algebra M).val - (U g : H →L[ℂ] H)‖ ≤ δ) :
    ∃ a : D → D → unitary (Algebra M),
      AEStronglyMeasurable (fun p : D × D => J (a p.1 p.2 : Algebra M)) (μ.prod μ) ∧
…

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

theorem OAI.KadisonKastler.StandardTracialPosition.exists_ae_diagonal_unitary_comparison line 224

Source documentation

The standard-position version needs only measurable operator evaluations of the original cocycle. Its diagonal unitary field is likewise measurable on every vector of the ambient Hilbert space.

theorem StandardTracialPosition.exists_ae_diagonal_unitary_comparison
    (p : StandardTracialPosition M) (α : NonsingularAction G D μ)
    (W : G → D → unitary (Algebra M))
    (hW : ∀ g t, ∀ᵐ x ∂μ, (W (g * t) x : Algebra M) =
      (W g x : Algebra M) * (W t (α.toPerm g⁻¹ x) : Algebra M))
    (hWmeas : ∀ g ξ, AEStronglyMeasurable (fun x => (W g x : Algebra M).val ξ) μ)
    (U : G → unitary (H →L[ℂ] H)) {δ : ℝ} (hδ : 0 ≤ δ) (hsmall : 2 * δ < 1)
    (hclose : ∀ g, ∀ᵐ x ∂μ, ‖(W g x : Algebra M).val - (U g : H →L[ℂ] H)‖ ≤ δ) :
    ∃ a : D → D → unitary (Algebra M),
      (∀ ξ, AEStronglyMeasurable
        (fun x : D × D => (a x.1 x.2 : Algebra M).val ξ) (μ.prod μ)) ∧
      (∀ x y, ‖(a x y : Algebra M) - 1‖ ≤ 4 * δ) ∧
…

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