FixedComplementPaths.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Constant-complement paths for the concrete common-corner comparison

The path of the relative binary comparison stays in its actual corner. Combining it with fixed-support shrink paths gives a unitary path with the prescribed complementary isometry at every time. Its initial value is displayed literally; no connectedness of that initial value is assumed.

lemma OAI.WeakPureInfiniteness.exists_relative_binary_power_path line 22

Source documentation

Keep the path inside the common corner rather than forgetting its relative identity component when passing to the ambient algebra.

lemma exists_relative_binary_power_path
    (q : E) (hq : star q = q) (hqq : q * q = q) (hq0 : q ≠ 0)
    (a b : Fin 2 → E)
    (ha : ∀ i j, star (a i) * a j = if i = j then q else 0)
    (hb : ∀ i j, star (b i) * b j = if i = j then q else 0)
    (has : (∑ i, a i * star (a i)) = q)
    (hbs : (∑ i, b i * star (b i)) = q)
    (hab : bergRowsCommute a b) (m : ℕ) (ε : ℝ) (hε : 0 < ε) :
    ∃ V : unitInterval → unitary E, Continuous V ∧ V 0 = 1 ∧
      (∀ t, (V t : E) * (1 - q) = 1 - q ∧ (1 - q) * (V t : E) = 1 - q) ∧
      ∀ i ≤ m, ‖(V 1 : E) * (a 0 ^ i * a 1) * star (V 1 : E) -
        (b 0 ^ i * b 1)‖ < ε := by
…

Mentions: OAI.WeakPureInfiniteness.bergRowsCommute

lemma OAI.WeakPureInfiniteness.exists_commonCorner_fixedComplement_path line 77

Source documentation

Constant initial/final projections and a corner-preserving comparison give an actual continuous family of the prescribed complementary extensions.

lemma exists_commonCorner_fixedComplement_path
    (q p R w z : E) (hq : star q = q) (hp : star p = p)
    (hw : star w * w = 1) (hww : w * star w = 1 - q)
    (hz : star z * z = 1) (hzz : z * star z = 1 - p)
    (c d : unitInterval → E) (hc : Continuous c) (hd : Continuous d)
    (hcg : ∀ t, star (c t) * c t = q)
    (hcr : ∀ t, c t * star (c t) = R)
    (hcq : ∀ t, c t * q = c t)
    (hdg : ∀ t, star (d t) * d t = p)
    (hdr : ∀ t, d t * star (d t) = R)
    (hdp : ∀ t, d t * p = d t)
    (V : unitInterval → unitary E) (hV : Continuous V) (hV0 : V 0 = 1)
…

lemma OAI.WeakPureInfiniteness.fixedComplement_path_product line 122

Source documentation

Two such paths with the same complementary action cancel that action exactly. Connectedness reduces to their literal initial product.

lemma fixedComplement_path_product
    (U V : unitInterval → unitary E) (hU : Continuous U) (hV : Continuous V)
    (w z : E) (hUw : ∀ t, (U t : E) * w = z) (hVw : ∀ t, (V t : E) * w = z) :
    Continuous (fun t => star (V t) * U t) ∧
      (∀ t, ((star (V t) * U t : unitary E) : E) * w = w) ∧
      Joined (star (V 0) * U 0) (star (V 1) * U 1) := by
…