BoundaryImprovement.lean`

20 declarations, 0 contain sorry, 0 declared as axioms

The quadratic step in boundary cocycle correction

Only the structural properties of the boundary mean occur here. The mean need not be normal. Covariance cancellation and polar normalization give the quadratic improvement used in the measurable iteration.

structure OAI.KadisonKastler.BimoduleMean line 25
Source documentation
A contractive, unital, star-preserving mean with both module identities. The map ι includes fields independent of the averaged variable.
```
structure BimoduleMean (ι : B →⋆ₐ[ℂ] A) where
…
```
theorem OAI.KadisonKastler.BimoduleMean.fixed line 38

theorem OAI.KadisonKastler.BimoduleMean.covariance line 42

Source documentation

The linear terms cancel exactly in the centered product.

theorem covariance (x y : A) :
    m.toCLM (x * y) - m.toCLM x * m.toCLM y =
      m.toCLM ((x - ι (m.toCLM x)) * (y - ι (m.toCLM y))) := by
…

theorem OAI.KadisonKastler.BimoduleMean.norm_covariance_le line 49

Source documentation

Contractivity of the mean bounds the covariance by its two residuals.

theorem norm_covariance_le (x y : A) :
    ‖m.toCLM (x * y) - m.toCLM x * m.toCLM y‖ ≤
      ‖x - ι (m.toCLM x)‖ * ‖y - ι (m.toCLM y)‖ := by
…

theorem OAI.KadisonKastler.BimoduleMean.variance line 56

Source documentation

For a unitary the covariance identity is the exact unitarity defect.

theorem variance (x : unitary A) :
    1 - star (m.toCLM (x : A)) * m.toCLM (x : A) =
      m.toCLM (star ((x : A) - ι (m.toCLM (x : A))) *
        ((x : A) - ι (m.toCLM (x : A)))) := by
…

theorem OAI.KadisonKastler.BimoduleMean.norm_sub_le line 69
Source documentation
Averaging preserves the error from a field independent of the mean variable.
```
theorem norm_sub_le (x : A) (b : B) {e : ℝ} (h : ‖x - ι b‖ ≤ e) :
    ‖m.toCLM x - b‖ ≤ e := by
…
```
theorem OAI.KadisonKastler.BimoduleMean.norm_residual_le line 75
Source documentation
The residual from the average is at most twice the original error.
```
theorem norm_residual_le (x : A) (b : B) {e : ℝ} (h : ‖x - ι b‖ ≤ e) :
    ‖x - ι (m.toCLM x)‖ ≤ 2 * e := by
…
```

theorem OAI.KadisonKastler.BimoduleMean.norm_covariance_le_four_mul_sq line 87

Source documentation

Two residuals bounded by 2e give the quadratic covariance bound.

theorem norm_covariance_le_four_mul_sq (x y : A) {e : ℝ} (he : 0 ≤ e)
    (hx : ‖x - ι (m.toCLM x)‖ ≤ 2 * e)
    (hy : ‖y - ι (m.toCLM y)‖ ≤ 2 * e) :
    ‖m.toCLM (x * y) - m.toCLM x * m.toCLM y‖ ≤ 4 * e ^ 2 := by
…

theorem OAI.KadisonKastler.BimoduleMean.norm_variance_le_four_mul_sq line 98

Source documentation

The average of a unitary within e of the fixed algebra has unitarity error at most 4e².

theorem norm_variance_le_four_mul_sq (x : unitary A) (b : B) {e : ℝ}
    (he : 0 ≤ e) (hx : ‖(x : A) - ι b‖ ≤ e) :
    ‖1 - star (m.toCLM (x : A)) * m.toCLM (x : A)‖ ≤ 4 * e ^ 2 := by
…

theorem OAI.KadisonKastler.boundary_sqrt_scalar_sub_one_sq_le line 116
theorem OAI.KadisonKastler.norm_sqrt_sub_one_le line 129
Source documentation
The square root cannot increase the operator-norm error from one.
```
theorem norm_sqrt_sub_one_le (a : B) (ha : 0 ≤ a) :
    ‖CFC.sqrt a - 1‖ ≤ ‖a - 1‖ := by
…
```

theorem OAI.KadisonKastler.exists_polar_unitary_close_of_near_unitary line 158

Source documentation

Polar normalization costs no more than the unitarity defect.

theorem exists_polar_unitary_close_of_near_unitary (x : B) (v : unitary B)
    (hx : ‖x - (v : B)‖ < 1) :
    ∃ u : unitary B, (u : B) * CFC.abs x = x ∧
      ‖(u : B) - x‖ ≤ ‖star x * x - 1‖ := by
…

theorem OAI.KadisonKastler.norm_unitary_le_one line 180
Source documentation
A unitary is a contraction, including in the degenerate C-star algebra.
```
theorem norm_unitary_le_one (x : unitary A) : ‖(x : A)‖ ≤ 1 := by
…
```
def OAI.KadisonKastler.boundaryTransport line 189
Source documentation
The transport field used before averaging an approximate cocycle.
```
def boundaryTransport (α : G →* (B ≃⋆ₐ[ℂ] B)) (V : G → unitary B) (g t : G) : B :=
…
```
theorem OAI.KadisonKastler.boundaryTransport_mem_unitary line 193
Source documentation
The transport fields are unitary before averaging.
```
theorem boundaryTransport_mem_unitary (α : G →* (B ≃⋆ₐ[ℂ] B))
    (V : G → unitary B) (g t : G) : boundaryTransport α V g t ∈ unitary B := by
…
```
Mentions: OAI.KadisonKastler.boundaryTransport

theorem OAI.KadisonKastler.boundaryTransport_factor line 200

Source documentation

The transport construction has an exact factorization even when V is only an approximate cocycle.

theorem boundaryTransport_factor (α : G →* (B ≃⋆ₐ[ℂ] B))
    (V : G → unitary B) (g h t : G) :
    boundaryTransport α V (g * h) t =
      boundaryTransport α V g t * α g (boundaryTransport α V h (g⁻¹ * t)) := by
…

Mentions: OAI.KadisonKastler.boundaryTransport

theorem OAI.KadisonKastler.norm_boundaryTransport_sub_le line 211

Source documentation

The pointwise distance from the transport field to the original unitary is bounded by the original cocycle defect.

theorem norm_boundaryTransport_sub_le (α : G →* (B ≃⋆ₐ[ℂ] B))
    (V : G → unitary B) {e : ℝ}
    (hdefect : ∀ g h, ‖(V g : B) * α g (V h : B) - (V (g * h) : B)‖ ≤ e)
    (g t : G) : ‖boundaryTransport α V g t - (V g : B)‖ ≤ e := by
…

Mentions: OAI.KadisonKastler.boundaryTransport

theorem OAI.KadisonKastler.BimoduleMean.exists_improved_unitary line 240

Source documentation

One averaged unitary can be replaced by an actual unitary at quadratic cost, while retaining its original first-order proximity.

theorem BimoduleMean.exists_improved_unitary (X : unitary A) (V : unitary B)
    {e : ℝ} (he : 0 ≤ e) (he1 : e < 1) (hXV : ‖(X : A) - ι (V : B)‖ ≤ e) :
    ∃ W : unitary B,
      ‖(W : B) - m.toCLM (X : A)‖ ≤ 4 * e ^ 2 ∧
      ‖(W : B) - (V : B)‖ ≤ e + 4 * e ^ 2 := by
…

theorem OAI.KadisonKastler.BimoduleMean.norm_averaged_defect_le_four_mul_sq line 256

Source documentation

The operator-norm defect of the averaged family is quadratic.

theorem BimoduleMean.norm_averaged_defect_le_four_mul_sq
    {G : Type*} [Group G]
    (α : G → B ≃⋆ₐ[ℂ] B) (fieldAction : G → A ≃⋆ₐ[ℂ] A)
    (hequiv : ∀ g x, m.toCLM (fieldAction g x) = α g (m.toCLM x))
    (hι : ∀ g b, fieldAction g (ι b) = ι (α g b))
    (X : G → unitary A) (V : G → unitary B)
    (hfactor : ∀ g h, (X (g * h) : A) = (X g : A) * fieldAction g (X h : A))
    {e : ℝ} (he : 0 ≤ e) (hXV : ∀ g, ‖(X g : A) - ι (V g : B)‖ ≤ e)
    (g h : G) :
    ‖m.toCLM (X (g * h) : A) -
      m.toCLM (X g : A) * α g (m.toCLM (X h : A))‖ ≤ 4 * e ^ 2 := by
…

theorem OAI.KadisonKastler.BimoduleMean.exists_quadratic_improvement line 276

Source documentation

Quadratic polar correction for the entire family. The cocycle factorization and equivariance are exact structural identities; no correction conclusion is assumed.

theorem BimoduleMean.exists_quadratic_improvement
    {G : Type*} [Group G]
    (α : G → B ≃⋆ₐ[ℂ] B) (fieldAction : G → A ≃⋆ₐ[ℂ] A)
    (hequiv : ∀ g x, m.toCLM (fieldAction g x) = α g (m.toCLM x))
    (hι : ∀ g b, fieldAction g (ι b) = ι (α g b))
    (X : G → unitary A) (V : G → unitary B)
    (hfactor : ∀ g h, (X (g * h) : A) = (X g : A) * fieldAction g (X h : A))
    {e : ℝ} (he : 0 ≤ e) (he1 : e < 1)
    (hXV : ∀ g, ‖(X g : A) - ι (V g : B)‖ ≤ e) :
    ∃ W : G → unitary B,
      (∀ g, ‖(W g : B) - (V g : B)‖ ≤ e + 4 * e ^ 2) ∧
      (∀ g h, ‖(W g : B) * α g (W h : B) - (W (g * h) : B)‖ ≤ 16 * e ^ 2) := by
…