TracialHaarPerturbation.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Quantitative proximity in Haar symmetrization. The finite-factor argument uses a cluster point within the original scalar commutator bound.

theorem OAI.KadisonSimilarity.norm_weakOperatorIntegral_sub_le line 19

Source documentation

A weak integral stays in every operator norm ball containing its field.

theorem norm_weakOperatorIntegral_sub_le (A : X → H →L[ℂ] H)
    (hA : WeaklyIntegrable μ A) (R : ℝ) (hbound : ∀ g, ‖A g‖ ≤ R)
    (T : H →L[ℂ] H) {δ : ℝ} (hδ : 0 ≤ δ) (hclose : ∀ g, ‖A g - T‖ ≤ δ) :
    ‖weakOperatorIntegral μ A hA R hbound - T‖ ≤ δ := by
…

Mentions: OAI.KadisonSimilarity.WeaklyIntegrable, OAI.KadisonSimilarity.weakOperatorIntegral

theorem OAI.KadisonSimilarity.norm_unitaryConjugate_sub_le line 49
Source documentation
Conjugating by a contractive group representation moves an operator by at most its commutator with the group element.
```
theorem norm_unitaryConjugate_sub_le (U : Γ →* (H →L[ℂ] H))
    (hU : ∀ g, ‖U g‖ ≤ 1) (T : H →L[ℂ] H) {δ : ℝ}
    (hcomm : ∀ g, ‖commutator T (U g)‖ ≤ δ) (g : Γ) :
    ‖unitaryConjugate U T g - T‖ ≤ δ := by
…
```
Mentions: OAI.KadisonSimilarity.commutator, OAI.KadisonSimilarity.unitaryConjugate

theorem OAI.KadisonSimilarity.norm_haarTwirl_sub_le line 65

Source documentation

The Haar average is close to the original operator by the scalar bound.

theorem norm_haarTwirl_sub_le (ν : Measure Γ) [IsProbabilityMeasure ν]
    (U : Γ →* (H →L[ℂ] H)) (hU : ∀ g, ‖U g‖ ≤ 1)
    (T : H →L[ℂ] H) (hI : WeaklyIntegrable ν (unitaryConjugate U T))
    {δ : ℝ} (hδ : 0 ≤ δ) (hcomm : ∀ g, ‖commutator T (U g)‖ ≤ δ) :
    ‖haarTwirl ν U hU T hI - T‖ ≤ δ :=
…

Mentions: OAI.KadisonSimilarity.WeaklyIntegrable, OAI.KadisonSimilarity.unitaryConjugate, OAI.KadisonSimilarity.commutator, OAI.KadisonSimilarity.haarTwirl

theorem OAI.KadisonSimilarity.scalarCommutatorNorm_le_of_close line 74

Source documentation

The norm perturbation controls the full scalar commutator seminorm.

theorem scalarCommutatorNorm_le_of_close (P : VonNeumannAlgebra H)
    (S T : H →L[ℂ] H) {δ : ℝ} (hclose : ‖S - T‖ ≤ δ) :
    scalarCommutatorNorm P S ≤ scalarCommutatorNorm P T + 2 * δ := by
…

Mentions: OAI.KadisonSimilarity.scalarCommutatorNorm

theorem OAI.KadisonSimilarity.exists_simultaneously_symmetrized_close line 93

Source documentation

Increasing Haar averages give a single invariant operator within the original commutator bound. There is no invariant operator among the inputs.

theorem exists_simultaneously_symmetrized_close
    (U : ∀ n, G n →* (H →L[ℂ] H)) (hU : ∀ n g, ‖U n g‖ ≤ 1)
    (embedding : ∀ n m, n ≤ m → G n → G m)
    (hcompat : ∀ n m h g, U m (embedding n m h g) = U n g)
    (T : H →L[ℂ] H)
    (hI : ∀ n, WeaklyIntegrable (ν n) (unitaryConjugate (U n) T))
    {δ : ℝ} (hδ : 0 ≤ δ) (hcomm : ∀ n g, ‖commutator T (U n g)‖ ≤ δ) :
    ∃ S : H →L[ℂ] H, ‖S‖ ≤ ‖T‖ ∧ ‖S - T‖ ≤ δ ∧
      ∀ n g, commutator S (U n g) = 0 := by
…

Mentions: OAI.KadisonSimilarity.WeaklyIntegrable, OAI.KadisonSimilarity.unitaryConjugate, OAI.KadisonSimilarity.commutator

theorem OAI.KadisonSimilarity.exists_scalar_symmetrization line 120

Source documentation

The finite-factor averaging step, including the factor-three scalar commutator bound used before passage to the ultrapower.

theorem exists_scalar_symmetrization (P : VonNeumannAlgebra H)
    (U : ∀ n, G n →* (H →L[ℂ] H)) (hU : ∀ n g, ‖U n g‖ ≤ 1)
    (hmem : ∀ n g, U n g ∈ P)
    (embedding : ∀ n m, n ≤ m → G n → G m)
    (hcompat : ∀ n m h g, U m (embedding n m h g) = U n g)
    (T : H →L[ℂ] H)
    (hI : ∀ n, WeaklyIntegrable (ν n) (unitaryConjugate (U n) T)) :
    ∃ S : H →L[ℂ] H, ‖S‖ ≤ ‖T‖ ∧
      ‖S - T‖ ≤ scalarCommutatorNorm P T ∧
      scalarCommutatorNorm P S ≤ 3 * scalarCommutatorNorm P T ∧
      ∀ n g, commutator S (U n g) = 0 := by
…

Mentions: OAI.KadisonSimilarity.WeaklyIntegrable, OAI.KadisonSimilarity.unitaryConjugate, OAI.KadisonSimilarity.scalarCommutatorNorm, OAI.KadisonSimilarity.commutator