ShrinkPaths.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Paths of the actual inserted-unitary shrinks

The inverse canonical-shift implementer can be chosen in the identity component. Varying that implementer to one preserves both support projections of the shrink. This supplies a path to the literal base formula; the base fixed-complement extension is not asserted connected.

lemma OAI.WeakPureInfiniteness.exists_connected_canonicalShift_prefix_inverse line 22

Source documentation

Retain the connectedness supplied by the canonical-shift construction when passing to inverse conjugation and a finite encoded prefix.

lemma exists_connected_canonicalShift_prefix_inverse [Nontrivial E]
    (a : Fin 2 → E)
    (ha : ∀ i j, star (a i) * a j = if i = j then 1 else 0)
    (has : (∑ i, a i * star (a i)) = 1) (m : ℕ) (ε : ℝ) (hε : 0 < ε) :
    ∃ u : unitary E, Joined 1 u ∧ ∀ i ≤ m,
      ‖(u : E) * finiteRowShift a (a 0 ^ i * a 1) * star (u : E) -
        (a 0 ^ i * a 1)‖ < ε := by
…

Mentions: OAI.WeakPureInfiniteness.finiteRowShift

def OAI.WeakPureInfiniteness.binaryShrinkValue line 75
lemma OAI.WeakPureInfiniteness.binaryShrinkValue_continuous line 79
lemma OAI.WeakPureInfiniteness.binaryShrinkValue_one line 83

lemma OAI.WeakPureInfiniteness.exists_binary_shrink_path line 90

Source documentation

The actual shrink follows a continuous path with constant initial and final projections from its explicit base formula to the required estimate.

lemma exists_binary_shrink_path [Nontrivial E]
    (r a : Fin 2 → E)
    (hr : ∀ i j, star (r i) * r j = if i = j then 1 else 0)
    (ha : ∀ i j, star (a i) * a j = if i = j then 1 else 0)
    (has : (∑ i, a i * star (a i)) = 1)
    (hc : bergRowsCommute a r) (m : ℕ) (ε : ℝ) (hε : 0 < ε) :
    ∃ C : unitInterval → E, Continuous C ∧
      C 0 = binaryShrinkValue r a 1 ∧
      (∀ t, star (C t) * C t = 1 ∧ C t * star (C t) = 1 - r 0 * star (r 0)) ∧
      ∀ i ≤ m, ‖C 1 * (a 0 ^ i * a 1) * star (C 1) -
        (a 0 ^ i * a 1) * (1 - r 0 * star (r 0))‖ < ε := by
…

Mentions: OAI.WeakPureInfiniteness.bergRowsCommute, OAI.WeakPureInfiniteness.binaryShrinkValue

lemma OAI.WeakPureInfiniteness.exists_relative_binary_shrink_path line 120

Source documentation

The same actual deformation inside a projection corner, including both support equations at every time.

lemma exists_relative_binary_shrink_path
    (q : E) (hq : star q = q) (hqq : q * q = q) (hq0 : q ≠ 0)
    (r a : Fin 2 → E)
    (hrs : ∀ i, q * r i = r i ∧ r i * q = r i)
    (hasp : ∀ i, q * a i = a i ∧ a i * q = a i)
    (hr : ∀ i j, star (r i) * r j = if i = j then q else 0)
    (ha : ∀ i j, star (a i) * a j = if i = j then q else 0)
    (has : (∑ i, a i * star (a i)) = q)
    (hc : bergRowsCommute a r) (m : ℕ) (ε : ℝ) (hε : 0 < ε) :
    ∃ C : unitInterval → E, Continuous C ∧
      C 0 = q - star (finiteCuntzTransfer r a q) * finiteCuntzTransfer r a q +
        r 1 * finiteCuntzTransfer r a q ∧
…

Mentions: OAI.WeakPureInfiniteness.bergRowsCommute, OAI.WeakPureInfiniteness.finiteCuntzTransfer