NegativeGlobal.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Global comparison from the two concrete common-corner transfers

The transfer product has exact initial and final projections. Its norm estimate keeps all three errors, and a shared spare isometry permits the connected completion. The original canonical-generator transfer is separate.

lemma OAI.WeakPureInfiniteness.commonCornerTransfer_products line 20

Source documentation

Compose two transfers to the same corner with a unitary preserving it.

lemma commonCornerTransfer_products (P Q R c d : E) (u : unitary E)
    (hc : star c * c = P) (hcc : c * star c = R) (hcp : c * P = c)
    (hd : star d * d = Q) (hdd : d * star d = R) (hdq : d * Q = d)
    (hu : Commute (u : E) R) :
    let w := star d * (u : E) * c
…

lemma OAI.WeakPureInfiniteness.negativeGlobal_sandwich_norm line 49

lemma OAI.WeakPureInfiniteness.commonCornerTransfer_error line 61

Source documentation

No error is lost when pulling the three comparison errors back through contractive transfers.

lemma commonCornerTransfer_error (Q c d x y X Y : E) (u : unitary E)
    (hd : star d * d = Q) (hqy : Q * y = y) (hyq : y * Q = y)
    (hdn : ‖d‖ ≤ 1) (δ : ℝ)
    (hcx : ‖c * x * star c - X‖ < δ)
    (hdy : ‖d * y * star d - Y‖ < δ)
    (hu : ‖(u : E) * X * star (u : E) - Y‖ < δ) :
    let w := star d * (u : E) * c
…

lemma OAI.WeakPureInfiniteness.exists_canonicalNegative_global_comparison line 102

Source documentation

Full ambient comparison of the stabilized rows. The two original canonical rows themselves are not asserted to be conjugate here.

lemma exists_canonicalNegative_global_comparison [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 : bergRowsCommute s t) (m : ℕ) (ε : ℝ) (hε : 0 < ε) :
    ∃ u : unitary E, Joined (1 : unitary E) u ∧
      ∀ i ≤ m, ‖(u : E) * canonicalNegativeRow s i * star (u : E) -
        canonicalNegativeRow t i‖ < ε := by
…

Mentions: OAI.WeakPureInfiniteness.bergRowsCommute, OAI.WeakPureInfiniteness.canonicalNegativeRow