ProperBufferAbsorption.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Connected absorption of an arbitrary finite proper row

The target row is completed inside the zero-unit buffer corner. Only the prescribed original entries must commute with the binary buffer; the auxiliary completing entry is never included in that requirement.

lemma OAI.WeakPureInfiniteness.BufferAbsorptionCorner.exists_finite_absorption_on line 25

Source documentation

The finite Fock estimate only needs coefficient commutation at the indices at which an intertwining estimate is requested.

lemma BufferAbsorptionCorner.exists_finite_absorption_on [Nontrivial E]
    (D : BufferAbsorptionCorner E) (s t : I → E) (r : E) (P : I → Prop)
    (hrr : star r * r = 1) (hr : ∀ i, star r * s i = 0)
    (hs : ∀ i j, star (s i) * s j = if i = j then 1 else 0)
    (hqr : Commute D.q r) (hqs : ∀ i, Commute D.q (s i))
    (htq : ∀ i, t i * D.q = t i) (ht : ∑ i, t i * star (t i) = D.q)
    (htt : ∀ i j, star (t i) * t j = if i = j then D.q else 0)
    (hat : ∀ i, P i → Commute (star D.a) (t i))
    (hbt : ∀ i, P i → Commute (star D.b) (t i))
    (ε : ℝ) (hε : 0 < ε) :
    ∃ W : unitary E, Joined D.anchor W ∧
      ∀ i, P i → ‖(W : E) * s i - (t i + D.w * s i * star D.w) * (W : E)‖ < ε := by
…

Mentions: OAI.WeakPureInfiniteness.BufferAbsorptionCorner

lemma OAI.WeakPureInfiniteness.BufferAbsorptionCorner.extend_finite_proper_row line 90

lemma OAI.WeakPureInfiniteness.exists_connected_proper_buffer_absorption line 151

Source documentation

Connected absorption of any finite original proper-row prefix. The complementary source row remains as an explicit summand.

lemma exists_connected_proper_buffer_absorption [Nontrivial E]
    (s t r : ℕ → 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)
    (hr : ∀ i j, star (r i) * r j = if i = j then 1 else 0)
    (hrs : bergRowsCommute r s) (hrt : bergRowsCommute r t)
    (n : ℕ) (ε : ℝ) (hε : 0 < ε) :
    ∃ U : unitary E, Joined (1 : unitary E) U ∧
      ∀ i : Fin n,
        ‖(U : E) * s i * star (U : E) -
          (t i * (1 - r 0 * star (r 0)) + s i * (r 0 * star (r 0)))‖ < ε := by
…

Mentions: OAI.WeakPureInfiniteness.bergRowsCommute