BufferedIteration.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Iterating the concrete buffered absorption

The successive conjugacies move the residual representation into powers of the complementary isometry. Both the accumulated error and the entire terminal representation are retained. No norm decay is assigned to the terminal projection.

def OAI.WeakPureInfiniteness.bufferedAbsorptionValue line 21
Source documentation
The exact target after n buffered absorptions.
```
def bufferedAbsorptionValue (w t x : E) (n : ℕ) : E :=
…
```
lemma OAI.WeakPureInfiniteness.bufferedAbsorptionValue_zero line 24
lemma OAI.WeakPureInfiniteness.bufferedAbsorptionValue_one line 29
lemma OAI.WeakPureInfiniteness.bufferedAbsorptionValue_succ line 33

lemma OAI.WeakPureInfiniteness.bufferedAbsorption_conjugate line 48

Source documentation

The inner conjugation used at the next absorption step.

lemma bufferedAbsorption_conjugate (w t x : E) (hw : star w * w = 1)
    (htw : Commute t w) (htsw : Commute t (star w)) (v : unitary E) :
    (binaryCornerUnitary w hw v : E) *
        (t * (1 - w * star w) + w * x * star w) *
        star (binaryCornerUnitary w hw v : E) =
      t * (1 - w * star w) + w * ((v : E) * x * star (v : E)) * star w := by
…

Mentions: OAI.WeakPureInfiniteness.binaryCornerUnitary

lemma OAI.WeakPureInfiniteness.buffered_sandwich_norm line 89

lemma OAI.WeakPureInfiniteness.exists_connected_buffered_iteration line 108

Source documentation

Repeated absorption is implemented by actual connected unitaries. The error is at most m * ε; its target keeps the full terminal copy.

lemma exists_connected_buffered_iteration {I : Type*}
    (s t : I → E) (w : E) (hw : star w * w = 1)
    (htw : ∀ i, Commute (t i) w) (htsw : ∀ i, Commute (t i) (star w))
    (u : unitary E) (hu : Joined (1 : unitary E) u)
    (ε : ℝ)
    (he : ∀ i, ‖(u : E) * s i * star (u : E) -
      bufferedAbsorptionValue w (t i) (s i) 1‖ ≤ ε)
    (m : ℕ) :
    ∃ v : unitary E, Joined (1 : unitary E) v ∧
      ∀ i, ‖(v : E) * s i * star (v : E) -
        bufferedAbsorptionValue w (t i) (s i) m‖ ≤ m * ε := by
…

Mentions: OAI.WeakPureInfiniteness.bufferedAbsorptionValue

lemma OAI.WeakPureInfiniteness.exists_canonical_buffered_iterations line 165

Source documentation

One actual source corner works at every finite iteration depth. The chosen unitary depends on the depth and requested final error.

lemma exists_canonical_buffered_iterations [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)
    (hst : bergRowsCommute s t) (n : ℕ) (κ : ℝ) (hκ : 0 < κ) :
    ∃ D : BufferAbsorptionCorner E,
      D.q ≠ 0 ∧
      (∀ i : Fin (n + 1), ‖s i * D.q - D.q * s i‖ < κ) ∧
      (∀ i : Fin (n + 1),
        ‖D.q * s i * D.q - zeroCornerRow D.q D.a D.b n i‖ < κ) ∧
      ∀ (m : ℕ) (ε : ℝ), 0 < ε →
        ∃ v : unitary E, Joined (1 : unitary E) v ∧
…

Mentions: OAI.WeakPureInfiniteness.bergRowsCommute, OAI.WeakPureInfiniteness.BufferAbsorptionCorner, OAI.WeakPureInfiniteness.zeroCornerRow