WeakCPDescent.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

From finite coefficient approximations to an original-space unitary

The unitary family may vary freely with the finite tests. Its pointwise weak ultralimit is UCP, retains the complete bound, and has range in the neighboring von Neumann algebra. This is the limit step in Section 9.

theorem OAI.KadisonKastler.complete_conjugation_restriction line 30
Source documentation
Conjugations with a uniform displacement bound have the corresponding uniform complete bound on every concrete subalgebra.
```
theorem complete_conjugation_restriction (u : unitary (H →L[ℂ] H)) :
    CompletelyBoundedBy
      ((unitaryConjugationLinear u).comp (algebraInclusion M).toAlgHom.toLinearMap -
        (algebraInclusion M).toAlgHom.toLinearMap) (2 * ‖(u : H →L[ℂ] H) - 1‖) := by
…
```
Mentions: OAI.KadisonKastler.CompletelyBoundedBy, OAI.KadisonKastler.unitaryConjugationLinear, OAI.KadisonKastler.algebraInclusion

theorem OAI.KadisonKastler.concrete_unitary_of_weak_conjugations line 41

Source documentation

An arbitrarily varying family of nearby conjugations suffices, provided each fixed coefficient is asymptotically approximated by the neighbor.

theorem concrete_unitary_of_weak_conjugations
    (hCorrection : PublishedMultiplicationCorrection M)
    (hCommutant : PublishedBlockCommutantApproximation (Algebra M) H)
    (ω : Ultrafilter ι) (U : ι → unitary (H →L[ℂ] H))
    {a g : ℝ} (ha : 0 ≤ a) (hU : ∀ i, ‖(U i : H →L[ℂ] H) - 1‖ ≤ a)
    (b : ι → Algebra M → Algebra N)
    (hb : ∀ x : Algebra M, ∀ ξ η : H,
      Tendsto (fun i => inner ℂ η
        (((b i x : H →L[ℂ] H) -
          (U i : H →L[ℂ] H) * (x : H →L[ℂ] H) * star (U i : H →L[ℂ] H)) ξ))
        (ω : Filter ι) (𝓝 0))
    (hsmall : 2 * a < 1 / 1000) (hge : g + 2 * a < 1)
…

Mentions: OAI.KadisonKastler.PublishedMultiplicationCorrection, OAI.KadisonKastler.PublishedBlockCommutantApproximation, OAI.KadisonKastler.Algebra