ConnectedGeneratorWitness.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Connected finite conjugacy of the two actual O∞ images

The first buffer is constructed from the two commuting images. The entire tail cancellation takes place in its closed commutant and the second norm ultrapower. Two connected-unitary descents give the original finite witness.

lemma OAI.WeakPureInfiniteness.generatorWitness_quotient_nontrivial line 21

theorem OAI.WeakPureInfiniteness.oInfinity_connected_generator_conjugacy line 39

Source documentation

All buffers, complement matching, and connected coordinate lifts are constructed from the two given commuting unital images.

theorem oInfinity_connected_generator_conjugacy [Nontrivial E]
    (U : Ultrafilter ℕ) [Fact ((U : Filter ℕ) ≤ atTop)]
    (f g : OInfinity →⋆ₐ[ℂ] E) (hfg : ∀ x y, Commute (f x) (g y))
    (n : ℕ) (ε : ℝ) (hε : 0 < ε) :
    ∃ v : unitary E, Joined 1 v ∧
      ∀ i < n, ‖(v : E) * f (oInfinityIsometry i) * star (v : E) -
        g (oInfinityIsometry i)‖ < ε := by
…

Mentions: OAI.WeakPureInfiniteness.OInfinity, OAI.WeakPureInfiniteness.oInfinityIsometry