BoundaryIntertwiner.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Averaging and polar normalization of a boundary intertwiner

A supplied equivariant bimodule mean gives a near-identity semilinear intertwiner. Continuous functional calculus passes its transformation law to the unitary polar factor.

theorem OAI.KadisonKastler.abs_unitary_mul line 27
Source documentation
Left multiplication by a unitary does not change the absolute value.
```
theorem abs_unitary_mul (u : unitary B) (b : B) :
    CFC.abs ((u : B) * b) = CFC.abs b := by
…
```
theorem OAI.KadisonKastler.abs_mul_unitary line 39
Source documentation
Right multiplication by a unitary conjugates the absolute value.
```
theorem abs_mul_unitary (b : B) (u : unitary B) :
    CFC.abs (b * (u : B)) = star (u : B) * CFC.abs b * (u : B) := by
…
```

theorem OAI.KadisonKastler.abs_semilinear_intertwines line 51

Source documentation

The absolute value satisfies the semilinear covariance forced by an invertible intertwiner of unitaries.

theorem abs_semilinear_intertwines (a : B ≃⋆ₐ[ℂ] B) (b : B)
    (u v : unitary B) (hb : b * (u : B) = (v : B) * a b) :
    CFC.abs b * (u : B) = (u : B) * a (CFC.abs b) := by
…

theorem OAI.KadisonKastler.polar_unitary_semilinear_intertwines line 67

Source documentation

An invertible semilinear intertwiner passes its law to its polar unitary.

theorem polar_unitary_semilinear_intertwines (a : B ≃⋆ₐ[ℂ] B) (b : B)
    (hunit : IsUnit b) (u v L : unitary B)
    (hb : b * (u : B) = (v : B) * a b)
    (hL : (L : B) * CFC.abs b = b) :
    (L : B) * (u : B) = (v : B) * a (L : B) := by
…

theorem OAI.KadisonKastler.averaged_boundary_intertwiner line 90
Source documentation
Averaging the genuine field S_t U_t* produces the semilinear intertwiner.
```
theorem averaged_boundary_intertwiner
    (α : G →* (B ≃⋆ₐ[ℂ] B))
    (m : BimoduleMean (boundaryConstant (G := G) (B := B)))
…
```
Mentions: OAI.KadisonKastler.BimoduleMean, OAI.KadisonKastler.boundaryConstant
theorem OAI.KadisonKastler.exists_unitary_boundary_intertwiner line 135
Source documentation
The averaged boundary intertwiner has a near-identity unitary polar factor satisfying the same semilinear intertwining equation.
```
theorem exists_unitary_boundary_intertwiner
    (α : G →* (B ≃⋆ₐ[ℂ] B))
    (m : BimoduleMean (boundaryConstant (G := G) (B := B)))
…
```
Mentions: OAI.KadisonKastler.BimoduleMean, OAI.KadisonKastler.boundaryConstant