BufferAbsorption.lean`

32 declarations, 0 contain sorry, 0 declared as axioms

An ambient unitary for finite-row absorption

A coisometric binary row in a corner and an isometry onto its complement give an explicit ambient unitary. Applied to the finite Fock isometry, this unitary absorbs the coisometric target row with a vanishing error. Its path component is recorded by an explicit, fixed anchor; connectedness of that anchor is not inferred from the corner relations.

structure OAI.WeakPureInfiniteness.BufferAbsorptionCorner line 22
Source documentation
The exact corner data used by the absorption formula.
```
structure BufferAbsorptionCorner (E : Type*) [CStarAlgebra E] where
…
```
lemma OAI.WeakPureInfiniteness.BufferAbsorptionCorner.a_right line 40
lemma OAI.WeakPureInfiniteness.BufferAbsorptionCorner.b_right line 44
lemma OAI.WeakPureInfiniteness.BufferAbsorptionCorner.reverse_orthogonal line 48
lemma OAI.WeakPureInfiniteness.BufferAbsorptionCorner.a_left line 51
lemma OAI.WeakPureInfiniteness.BufferAbsorptionCorner.b_left line 55
lemma OAI.WeakPureInfiniteness.BufferAbsorptionCorner.a_star_right line 59
lemma OAI.WeakPureInfiniteness.BufferAbsorptionCorner.b_star_right line 63
lemma OAI.WeakPureInfiniteness.BufferAbsorptionCorner.a_star_left line 67
lemma OAI.WeakPureInfiniteness.BufferAbsorptionCorner.b_star_left line 71
lemma OAI.WeakPureInfiniteness.BufferAbsorptionCorner.a_w line 75
lemma OAI.WeakPureInfiniteness.BufferAbsorptionCorner.b_w line 78
lemma OAI.WeakPureInfiniteness.BufferAbsorptionCorner.a_star_w line 81
lemma OAI.WeakPureInfiniteness.BufferAbsorptionCorner.b_star_w line 84
def OAI.WeakPureInfiniteness.BufferAbsorptionCorner.remainder line 88
Source documentation
The coisometry filling the complement of the first binary range.
```
def remainder : E := star D.b + (1 - D.q)
```
lemma OAI.WeakPureInfiniteness.BufferAbsorptionCorner.remainder_gram line 90
lemma OAI.WeakPureInfiniteness.BufferAbsorptionCorner.remainder_range line 101
lemma OAI.WeakPureInfiniteness.BufferAbsorptionCorner.remainder_a line 111
def OAI.WeakPureInfiniteness.BufferAbsorptionCorner.rotationValue line 117
Source documentation
The fixed anchor and its deformation by an arbitrary ambient unitary.
```
def rotationValue (u : unitary E) : E :=
…
```
lemma OAI.WeakPureInfiniteness.BufferAbsorptionCorner.rotationValue_mem_unitary line 120
def OAI.WeakPureInfiniteness.BufferAbsorptionCorner.rotation line 169
def OAI.WeakPureInfiniteness.BufferAbsorptionCorner.anchor line 173
Source documentation
This value, rather than the identity, is the immediate path anchor.
```
def anchor : unitary E := D.rotation 1
```
def OAI.WeakPureInfiniteness.BufferAbsorptionCorner.absorption line 175
lemma OAI.WeakPureInfiniteness.BufferAbsorptionCorner.absorption_continuous line 177
lemma OAI.WeakPureInfiniteness.BufferAbsorptionCorner.absorption_joined_anchor line 184
lemma OAI.WeakPureInfiniteness.BufferAbsorptionCorner.absorption_expansion line 189
lemma OAI.WeakPureInfiniteness.BufferAbsorptionCorner.absorption_error_formula line 222
lemma OAI.WeakPureInfiniteness.BufferAbsorptionCorner.transported_commutator_bound line 263
lemma OAI.WeakPureInfiniteness.BufferAbsorptionCorner.absorption_error_bound line 286
lemma OAI.WeakPureInfiniteness.finiteRowWordSum_left_of_commute line 338
lemma OAI.WeakPureInfiniteness.finiteRowIsometry_left_of_commute line 359

lemma OAI.WeakPureInfiniteness.BufferAbsorptionCorner.exists_finite_absorption line 367

Source documentation

An actual ambient unitary absorbs a finite coisometric row. The unitary is connected to the fixed, explicit buffer anchor.

lemma BufferAbsorptionCorner.exists_finite_absorption [Nontrivial E]
    (D : BufferAbsorptionCorner E) (s t : I → E) (r : E)
    (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, Commute (star D.a) (t i))
    (hbt : ∀ i, Commute (star D.b) (t i))
    (ε : ℝ) (hε : 0 < ε) :
    ∃ W : unitary E, Joined D.anchor W ∧
      ∀ i, ‖(W : E) * s i - (t i + D.w * s i * star D.w) * (W : E)‖ < ε := by
…

Mentions: OAI.WeakPureInfiniteness.BufferAbsorptionCorner