BalancedOrbitFamilies.lean`

15 declarations, 0 contain sorry, 0 declared as axioms

Balanced two-sided unitary orbit families

Independent equal-weight left and right conjugation averages control the respective covariances of the Cartesian-product orbit family. Its common pairing is unchanged by an operator commuting with both unitary actions.

def OAI.KadisonKastler.twoSidedOrbit line 24
Source documentation
The finite two-sided orbit, indexed by independent choices.
```
def twoSidedOrbit (d : I → unitary A) (e : J → unitary A) (a : A) (ij : I × J) : A :=
…
```
theorem OAI.KadisonKastler.twoSidedUnitary_left_square line 27
theorem OAI.KadisonKastler.twoSidedUnitary_right_square line 36
theorem OAI.KadisonKastler.finiteAverage_product_fst line 46
theorem OAI.KadisonKastler.finiteAverage_product_snd line 59
theorem OAI.KadisonKastler.finiteSignLeftCovariance_eq_finiteAverage line 67
theorem OAI.KadisonKastler.finiteSignRightCovariance_eq_finiteAverage line 73
theorem OAI.KadisonKastler.twoSidedOrbit_left_covariance line 81
Source documentation
The right randomization disappears from the left covariance.
```
theorem twoSidedOrbit_left_covariance (d : I → unitary A) (e : J → unitary A) (a : A) :
    finiteSignLeftCovariance (twoSidedOrbit d e a) =
      finiteAverage (fun i => (d i : A) * (a * star a) * star (d i : A)) := by
…
```
Mentions: OAI.KadisonKastler.finiteSignLeftCovariance, OAI.KadisonKastler.twoSidedOrbit, OAI.KadisonKastler.finiteAverage
theorem OAI.KadisonKastler.twoSidedOrbit_right_covariance line 95
Source documentation
The left randomization disappears from the right covariance.
```
theorem twoSidedOrbit_right_covariance (d : I → unitary A) (e : J → unitary A) (a : A) :
    finiteSignRightCovariance (twoSidedOrbit d e a) =
      finiteAverage (fun j => star (e j : A) * (star a * a) * (e j : A)) := by
…
```
Mentions: OAI.KadisonKastler.finiteSignRightCovariance, OAI.KadisonKastler.twoSidedOrbit, OAI.KadisonKastler.finiteAverage
theorem OAI.KadisonKastler.twoSidedOrbit_twoNorm line 109
Source documentation
Each two-sided orbit point has exactly the original tracial two-norm.
```
theorem twoSidedOrbit_twoNorm (τ : FaithfulTracialState A)
    (d : I → unitary A) (e : J → unitary A) (a : A) (ij : I × J) :
    traceTwoNorm τ (twoSidedOrbit d e a ij) = traceTwoNorm τ a := by
…
```
Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.traceTwoNorm, OAI.KadisonKastler.twoSidedOrbit

theorem OAI.KadisonKastler.pairing_unitary_of_commute line 117

Source documentation

Commutation lets a common unitary action pass through a pairing.

private theorem pairing_unitary_of_commute (V : H →L[ℂ] H)
    (u : unitary (H →L[ℂ] H)) (hu : Commute V (u : H →L[ℂ] H)) (x y : H) :
    inner ℂ (V ((u : H →L[ℂ] H) x)) ((u : H →L[ℂ] H) y) = inner ℂ (V x) y := by
…

theorem OAI.KadisonKastler.twoSidedOrbit_pairing line 127

Source documentation

A bimodular operator has the same pairing at every two-sided orbit point.

theorem twoSidedOrbit_pairing (Φ : A →ₗ[ℂ] H) (V : H →L[ℂ] H)
    (d : I → unitary A) (e : J → unitary A)
    (L : I → unitary (H →L[ℂ] H)) (R : J → unitary (H →L[ℂ] H))
    (hL : ∀ i x, Φ ((d i : A) * x) = (L i : H →L[ℂ] H) (Φ x))
    (hR : ∀ j x, Φ (x * (e j : A)) = (R j : H →L[ℂ] H) (Φ x))
    (hVL : ∀ i, Commute V (L i : H →L[ℂ] H))
    (hVR : ∀ j, Commute V (R j : H →L[ℂ] H))
    (a b : A) (ij : I × J) :
    inner ℂ (V (Φ (twoSidedOrbit d e a ij))) (Φ (twoSidedOrbit d e b ij)) =
      inner ℂ (V (Φ a)) (Φ b) := by
…

Mentions: OAI.KadisonKastler.twoSidedOrbit

theorem OAI.KadisonKastler.finiteSignLeftCovariance_reindex line 142
theorem OAI.KadisonKastler.finiteSignRightCovariance_reindex line 151

theorem OAI.KadisonKastler.exists_balanced_orbit_families line 161

Source documentation

Separate finite averages yield exactly the finite families used by the bounded-ball test, with an ordinary Fin n index.

theorem exists_balanced_orbit_families (τ : FaithfulTracialState A)
    (Φ : A →ₗ[ℂ] H) (V : H →L[ℂ] H)
    (d : I → unitary A) (e : J → unitary A)
    (L : I → unitary (H →L[ℂ] H)) (R : J → unitary (H →L[ℂ] H))
    (hL : ∀ i x, Φ ((d i : A) * x) = (L i : H →L[ℂ] H) (Φ x))
    (hR : ∀ j x, Φ (x * (e j : A)) = (R j : H →L[ℂ] H) (Φ x))
    (hVL : ∀ i, Commute V (L i : H →L[ℂ] H))
    (hVR : ∀ j, Commute V (R j : H →L[ℂ] H))
    (a b : A) (ha : traceTwoNorm τ a ≤ 1) (hb : traceTwoNorm τ b ≤ 1)
    (hQa : traceTwoNorm τ (finiteAverage (fun j => star (e j : A) * (star a * a) * (e j : A))) ≤ 2)
    (hLa : traceTwoNorm τ (finiteAverage (fun i => (d i : A) * (a * star a) * star (d i : A))) ≤ 2)
    (hQb : traceTwoNorm τ (finiteAverage (fun j => star (e j : A) * (star b * b) * (e j : A))) ≤ 2)
…

Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.traceTwoNorm, OAI.KadisonKastler.finiteAverage