ProductBoundaryCocycle.lean`

15 declarations, 0 contain sorry, 0 declared as axioms

The two-sided product boundary cocycle

Standard tracial conjugation turns the second copy into a commuting right action. The resulting product cocycle is close to the product representation with the explicit error 2 * δ + 2 * κ.

theorem OAI.KadisonKastler.conjugationOperator_one line 22
theorem OAI.KadisonKastler.conjugationOperator_mul line 28
theorem OAI.KadisonKastler.conjugationOperator_sub line 36

def OAI.KadisonKastler.conjugationUnitaryHom line 42

Source documentation

The right-action operation is a homomorphism on the unitary group.

def conjugationUnitaryHom (J : H ≃ₗᵢ⋆[ℂ] H) (hJ : Function.Involutive J) :
    unitary (H →L[ℂ] H) →* unitary (H →L[ℂ] H) where
…

theorem OAI.KadisonKastler.norm_conjugationOperator line 54
Source documentation
Conjugation by a conjugate-linear isometry preserves the operator norm.
```
theorem norm_conjugationOperator (J : H ≃ₗᵢ⋆[ℂ] H) (hJ : Function.Involutive J)
    (a : H →L[ℂ] H) : ‖conjugationOperator J a‖ = ‖a‖ := by
…
```
Mentions: OAI.KadisonKastler.conjugationOperator
theorem OAI.KadisonKastler.norm_conjugationOperator_sub line 67

theorem OAI.KadisonKastler.norm_conjugationOperator_change_le line 74

Source documentation

Moving the two conjugations costs at most twice their distance.

theorem norm_conjugationOperator_change_le (J₁ J₂ : H ≃ₗᵢ⋆[ℂ] H)
    (a : H →L[ℂ] H) :
    ‖conjugationOperator J₁ a - conjugationOperator J₂ a‖ ≤
      2 * ‖(J₁ : H →L⋆[ℂ] H) - (J₂ : H →L⋆[ℂ] H)‖ * ‖a‖ := by
…

Mentions: OAI.KadisonKastler.conjugationOperator

theorem OAI.KadisonKastler.StandardTracialPosition.commute_conjugationOperator line 102
Source documentation
Left multiplication commutes with every tracial right multiplier.
```
theorem commute_conjugationOperator (a b : H →L[ℂ] H) (ha : a ∈ N) (hb : b ∈ N) :
    Commute a (conjugationOperator p.conjugation b) := by
…
```
Mentions: OAI.KadisonKastler.conjugationOperator

def OAI.KadisonKastler.productBoundaryValue line 113

Source documentation

The pointwise product of the left cocycle and its tracial right copy.

def productBoundaryValue {N : VonNeumannAlgebra H} (p : StandardTracialPosition N)
    (W : G → D → unitary (H →L[ℂ] H)) (g : G × G) (x : D × D) :
    unitary (H →L[ℂ] H) :=
…

Mentions: OAI.KadisonKastler.StandardTracialPosition

theorem OAI.KadisonKastler.productBoundaryValue_coe line 120

theorem OAI.KadisonKastler.productBoundaryValue_cocycle line 127

Source documentation

The two-sided field satisfies the product-action cocycle law.

theorem productBoundaryValue_cocycle {N : VonNeumannAlgebra H}
    (p : StandardTracialPosition N) (α : G →* Equiv.Perm D)
    (W : G → D → unitary (H →L[ℂ] H))
    (hmem : ∀ g x, (W g x : H →L[ℂ] H) ∈ N)
    (hcoc : ∀ g h x, (W (g * h) x : H →L[ℂ] H) =
      (W g x : H →L[ℂ] H) * (W h (α g⁻¹ x) : H →L[ℂ] H))
    (g h : G × G) (x : D × D) :
    (productBoundaryValue p W (g * h) x : H →L[ℂ] H) =
      (productBoundaryValue p W g x : H →L[ℂ] H) *
        (productBoundaryValue p W h (α g.1⁻¹ x.1, α g.2⁻¹ x.2) : H →L[ℂ] H) := by
…

Mentions: OAI.KadisonKastler.StandardTracialPosition, OAI.KadisonKastler.productBoundaryValue

def OAI.KadisonKastler.productBoundaryRepresentation line 149
Source documentation
The commuting left and right copies form an actual representation.
```
def productBoundaryRepresentation {M : VonNeumannAlgebra H}
    (p : StandardTracialPosition M) (U : G →* unitary (Algebra M)) :
    (G × G) →* unitary (H →L[ℂ] H) where
…
```
Mentions: OAI.KadisonKastler.StandardTracialPosition, OAI.KadisonKastler.Algebra
theorem OAI.KadisonKastler.productBoundaryRepresentation_coe line 183

theorem OAI.KadisonKastler.norm_product_conjugation_sub_le line 189

Source documentation

Perturbing two unitary factors and the conjugation has an additive bound.

theorem norm_product_conjugation_sub_le
    (J₁ J₂ : H ≃ₗᵢ⋆[ℂ] H) (hJ₂ : Function.Involutive J₂)
    (a b c d : unitary (H →L[ℂ] H))
    {δ κ : ℝ} (hδ : 0 ≤ δ) (hκ : 0 ≤ κ)
    (hab : ‖(a : H →L[ℂ] H) - b‖ ≤ δ)
    (hcd : ‖(c : H →L[ℂ] H) - d‖ ≤ δ)
    (hJ : ‖(J₁ : H →L⋆[ℂ] H) - (J₂ : H →L⋆[ℂ] H)‖ ≤ κ) :
    ‖(a : H →L[ℂ] H) * conjugationOperator J₂ c -
      (b : H →L[ℂ] H) * conjugationOperator J₁ d‖ ≤ 2 * δ + 2 * κ := by
…

Mentions: OAI.KadisonKastler.conjugationOperator

theorem OAI.KadisonKastler.productBoundaryValue_close line 232

Source documentation

Pointwise perturbation of a two-sided boundary field.

theorem productBoundaryValue_close {M N : VonNeumannAlgebra H}
    (pM : StandardTracialPosition M) (pN : StandardTracialPosition N)
    (U : G →* unitary (Algebra M)) (W : G → D → unitary (H →L[ℂ] H))
    {δ κ : ℝ} (hδ : 0 ≤ δ) (hκ : 0 ≤ κ)
    (hclose : ∀ g x, ‖(W g x : H →L[ℂ] H) - (U g : Algebra M).val‖ ≤ δ)
    (hJ : ‖(pM.conjugation : H →L⋆[ℂ] H) - (pN.conjugation : H →L⋆[ℂ] H)‖ ≤ κ)
    (g : G × G) (x : D × D) :
    ‖(productBoundaryValue pN W g x : H →L[ℂ] H) -
      (productBoundaryRepresentation pM U g : H →L[ℂ] H)‖ ≤ 2 * δ + 2 * κ := by
…

Mentions: OAI.KadisonKastler.StandardTracialPosition, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.productBoundaryValue, OAI.KadisonKastler.productBoundaryRepresentation