IncompleteBinaryPath.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Uniform paths for the actual incomplete binary cocycle

Binary fragmentation needs two orthogonal isometries, not a coisometric row. For the complemented binary corner map, the splitting defect of an iterated cocycle has a path controlled by the original one-step unitary. Thus the bound is independent of the number of cocycle factors. The binary family need not generate a dense subalgebra of O∞.

lemma OAI.WeakPureInfiniteness.incompleteUnitaryShift_sub_norm_le line 21
lemma OAI.WeakPureInfiniteness.incompleteUnitaryShift_binary line 30
def OAI.WeakPureInfiniteness.conjugateUnitaryShift line 44
lemma OAI.WeakPureInfiniteness.conjugateUnitaryShift_continuous line 50
lemma OAI.WeakPureInfiniteness.conjugateUnitaryShift_sub_norm_le line 55
lemma OAI.WeakPureInfiniteness.unitaryShift_iterate_sub_norm_le line 64

lemma OAI.WeakPureInfiniteness.exists_controlled_cocycle_splitting_path line 75

Source documentation

A fixed path for u controls the splitting defects of all its product cocycles. The two factors move simultaneously, so their speed is at most 2L.

lemma exists_controlled_cocycle_splitting_path (α : unitary E →* unitary E)
    (hαcont : Continuous α)
    (hα : ∀ x y, ‖(α x : E) - α y‖ ≤ ‖(x : E) - y‖)
    (u : unitary E) (L : ℝ) (p : Path (1 : unitary E) u)
    (hp : ∀ a b, ‖(p a : E) - p b‖ ≤ L * |(a : ℝ) - b|) (n : ℕ) :
    ∃ q : Path (1 : unitary E)
        (finiteGroupCocycle (G := unitary E) α u n *
…

Mentions: OAI.WeakPureInfiniteness.finiteGroupCocycle

lemma OAI.WeakPureInfiniteness.exists_uniform_incompleteBinaryCocycle_path line 113

Source documentation

Uniform contraction of the genuine complemented binary cocycle. In particular, no norm bound on the terminal projection enters this theorem.

lemma exists_uniform_incompleteBinaryCocycle_path (s : Fin 2 → E)
    (hs : ∀ i j, star (s i) * s j = if i = j then 1 else 0)
    (u : unitary E) (L : ℝ) (hL : 0 ≤ L) (p : Path (1 : unitary E) u)
    (hp : ∀ a b, ‖(p a : E) - p b‖ ≤ L * |(a : ℝ) - b|) (n : ℕ) :
    ∃ q : Path (finiteGroupCocycle (G := unitary E)
…

Mentions: OAI.WeakPureInfiniteness.finiteGroupCocycle

lemma OAI.WeakPureInfiniteness.exists_controlled_unitary_extension line 137

Source documentation

The explicit two-swap completion has a path of speed at most 4π. The bound does not depend on the rank of its initial projection.

lemma exists_controlled_unitary_extension [Nontrivial E] (v r : E)
    (hv : v * star v * v = v) (hr : star r * r = 1)
    (hpr : (star v * v) * r = 0) (hqr : (v * star v) * r = 0) :
    ∃ u : unitary E, (u : E) * (star v * v) = v ∧
      ∃ p : Path (1 : unitary E) u,
        ∀ a b, ‖(p a : E) - p b‖ ≤ (4 * Real.pi) * |(a : ℝ) - b| := by
…

lemma OAI.WeakPureInfiniteness.exists_controlled_row_transfer line 175

Source documentation

A supplied common unused isometry gives an actual one-step transfer with a path bound independent of the number of tested row entries.

lemma exists_controlled_row_transfer [Nontrivial E] (s t : I → E)
    (hs : ∀ i j, star (s i) * s j = if i = j then 1 else 0)
    (ht : ∀ i j, star (t i) * t j = if i = j then 1 else 0)
    (r : E) (hr : star r * r = 1)
    (hsr : ∀ i, star (s i) * r = 0) (htr : ∀ i, star (t i) * r = 0) :
    ∃ u : unitary E, (∀ i, (u : E) * s i = t i) ∧
      ∃ p : Path (1 : unitary E) u,
        ∀ a b, ‖(p a : E) - p b‖ ≤ (4 * Real.pi) * |(a : ℝ) - b| := by
…

lemma OAI.WeakPureInfiniteness.exists_controlled_canonical_transfer line 223

Source documentation

All canonical finite rows have a controlled one-step completion. The unused product generator supplies the common isometry explicitly.

lemma exists_controlled_canonical_transfer [Nontrivial E] (s t : ℕ → E)
    (hs : ∀ i j, star (s i) * s j = if i = j then 1 else 0)
    (ht : ∀ i j, star (t i) * t j = if i = j then 1 else 0)
    (hc : ∀ i j, Commute (star (t i)) (s j)) (N : ℕ) :
    ∃ u : unitary E, (∀ i < N, (u : E) * s i = t i) ∧
      ∃ p : Path (1 : unitary E) u,
        ∀ a b, ‖(p a : E) - p b‖ ≤ (4 * Real.pi) * |(a : ℝ) - b| := by
…

lemma OAI.WeakPureInfiniteness.exists_uniform_canonicalBinaryCocycle_paths line 251

Source documentation

Canonical binary cocycles have a uniform 320π path bound.

lemma exists_uniform_canonicalBinaryCocycle_paths [Nontrivial E] (s t : ℕ → E)
    (hs : ∀ i j, star (s i) * s j = if i = j then 1 else 0)
    (ht : ∀ i j, star (t i) * t j = if i = j then 1 else 0)
    (hc : ∀ i j, Commute (star (t i)) (s j)) :
    ∃ u : unitary E, (∀ i < 2, (u : E) * s i = t i) ∧
      ∀ n, ∃ p : Path (canonicalIncompleteCocycle s hs 2 u n) 1,
        ∀ a b, ‖(p a : E) - p b‖ ≤ (320 * Real.pi) * |(a : ℝ) - b| := by
…

Mentions: OAI.WeakPureInfiniteness.canonicalIncompleteCocycle