BoundaryBoundedTransport.lean`

15 declarations, 0 contain sorry, 0 declared as axioms

Bounded transport fields and the correction step

For an action on a C-star algebra, the transport fields are actual bounded unitary families. An equivariant bimodule mean therefore gives the quadratic step in the complete metric space of unitary families.

def OAI.KadisonKastler.boundaryConstant line 28
Source documentation
Fields independent of the averaged group coordinate.
```
def boundaryConstant : B →⋆ₐ[ℂ] (G →ᵇ B) where
…
```
theorem OAI.KadisonKastler.boundaryConstant_apply line 39
def OAI.KadisonKastler.boundaryTranslate line 44
Source documentation
Transport combines left translation of the group coordinate and the original action on the value algebra.
```
def boundaryTranslate (α : G →* (B ≃⋆ₐ[ℂ] B)) (g : G) :
    (G →ᵇ B) ≃⋆ₐ[ℂ] (G →ᵇ B) where
…
```
theorem OAI.KadisonKastler.boundaryTranslate_apply line 76
theorem OAI.KadisonKastler.boundaryTranslate_constant line 80
Source documentation
The translation action agrees with the original action on constant fields.
```
theorem boundaryTranslate_constant (α : G →* (B ≃⋆ₐ[ℂ] B)) (g : G) (b : B) :
    boundaryTranslate α g (boundaryConstant (G := G) b) =
…
```
Mentions: OAI.KadisonKastler.boundaryTranslate, OAI.KadisonKastler.boundaryConstant

def OAI.KadisonKastler.boundaryTranslationAction line 87

Source documentation

The induced translations themselves form a group action.

def boundaryTranslationAction (α : G →* (B ≃⋆ₐ[ℂ] B)) :
    G →* ((G →ᵇ B) ≃⋆ₐ[ℂ] (G →ᵇ B)) where
…

def OAI.KadisonKastler.boundedUnitaryFamily line 100
Source documentation
Any family of unitaries is uniformly bounded, hence defines an actual unitary of the bounded-function C-star algebra.
```
def boundedUnitaryFamily (V : G → unitary B) : unitary (G →ᵇ B) :=
…
```
theorem OAI.KadisonKastler.boundedUnitaryFamily_apply line 112
def OAI.KadisonKastler.boundedBoundaryTransport line 116
Source documentation
The exact transport field, bundled as a bounded unitary family.
```
def boundedBoundaryTransport (α : G →* (B ≃⋆ₐ[ℂ] B))
    (V : unitary (G →ᵇ B)) (g : G) : unitary (G →ᵇ B) :=
…
```
theorem OAI.KadisonKastler.boundedBoundaryTransport_apply line 123

theorem OAI.KadisonKastler.boundedBoundaryTransport_factor line 129

Source documentation

The exact pointwise transport factorization holds in the bounded algebra.

theorem boundedBoundaryTransport_factor (α : G →* (B ≃⋆ₐ[ℂ] B))
    (V : unitary (G →ᵇ B)) (g h : G) :
    (boundedBoundaryTransport α V (g * h) : G →ᵇ B) =
      (boundedBoundaryTransport α V g : G →ᵇ B) *
        boundaryTranslate α g (boundedBoundaryTransport α V h : G →ᵇ B) := by
…

Mentions: OAI.KadisonKastler.boundedBoundaryTransport, OAI.KadisonKastler.boundaryTranslate

theorem OAI.KadisonKastler.norm_unitaryCocycleError_le line 138

Source documentation

Each pointwise defect is bounded by its actual uniform norm.

theorem norm_unitaryCocycleError_le (α : G →* (B ≃⋆ₐ[ℂ] B))
    (V : unitary (G →ᵇ B)) (g h : G) :
    ‖V.val g * α g (V.val h) - V.val (g * h)‖ ≤ unitaryCocycleDefect α V :=
…

Mentions: OAI.KadisonKastler.unitaryCocycleDefect

theorem OAI.KadisonKastler.norm_boundedBoundaryTransport_sub_le line 145
Source documentation
The transport family is uniformly within the actual cocycle defect of its constant value at the given group element.
```
theorem norm_boundedBoundaryTransport_sub_le (α : G →* (B ≃⋆ₐ[ℂ] B))
    (V : unitary (G →ᵇ B)) (g : G) :
    ‖(boundedBoundaryTransport α V g : G →ᵇ B) -
      boundaryConstant (G := G) (V.val g)‖ ≤ unitaryCocycleDefect α V := by
…
```
Mentions: OAI.KadisonKastler.boundedBoundaryTransport, OAI.KadisonKastler.boundaryConstant, OAI.KadisonKastler.unitaryCocycleDefect
theorem OAI.KadisonKastler.exists_bounded_cocycle_improvement line 156
Source documentation
An equivariant bimodule mean gives the actual metric-space refinement, with the precise defect and displacement constants.
```
theorem exists_bounded_cocycle_improvement
    (α : G →* (B ≃⋆ₐ[ℂ] B))
    (m : BimoduleMean (boundaryConstant (G := G) (B := B)))
…
```
Mentions: OAI.KadisonKastler.BimoduleMean, OAI.KadisonKastler.boundaryConstant
theorem OAI.KadisonKastler.exists_bounded_cocycle_of_equivariant_mean line 185
Source documentation
Iterating the actual bounded-family step gives an exact cocycle. The sole averaging premise is the explicitly supplied equivariant mean.
```
theorem exists_bounded_cocycle_of_equivariant_mean
    (α : G →* (B ≃⋆ₐ[ℂ] B))
    (m : BimoduleMean (boundaryConstant (G := G) (B := B)))
…
```
Mentions: OAI.KadisonKastler.BimoduleMean, OAI.KadisonKastler.boundaryConstant