CocycleMetric.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

The cocycle defect is continuous for the uniform norm. This supplies the metric-space part of the boundary correction iteration.

def OAI.KadisonKastler.unitaryFamilyEval line 28
Source documentation
Evaluation of an actual uniformly bounded unitary family.
```
def unitaryFamilyEval (V : unitary (G →ᵇ B)) (g : G) : unitary B :=
…
```
def OAI.KadisonKastler.unitaryCocycleError line 37
Source documentation
The cocycle error as a bounded function of the two group variables.
```
def unitaryCocycleError (α : G →* (B ≃⋆ₐ[ℂ] B)) (V : unitary (G →ᵇ B)) :
    (G × G) →ᵇ B :=
…
```
def OAI.KadisonKastler.unitaryCocycleDefect line 54
Source documentation
The supremum of all cocycle errors.
```
def unitaryCocycleDefect (α : G →* (B ≃⋆ₐ[ℂ] B))
    (V : unitary (G →ᵇ B)) : ℝ := ‖unitaryCocycleError α V‖
```
Mentions: OAI.KadisonKastler.unitaryCocycleError
theorem OAI.KadisonKastler.unitaryCocycleDefect_nonneg line 57
theorem OAI.KadisonKastler.unitaryCocycleDefect_eq_zero_iff line 60
theorem OAI.KadisonKastler.unitary_cocycle_error_difference_le line 71
theorem OAI.KadisonKastler.unitaryCocycleError_lipschitz line 105
theorem OAI.KadisonKastler.continuous_unitaryCocycleDefect line 116