BufferedPaths.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Uniform paths for actual buffered iterates

The compression of every connected unitary fixes the same full isometry inside the complementary corner. The fixed-spare construction gives these compressions a uniform 9π path bound. The resulting iterates have a bound independent of depth, with the fixed base path cost retained. Their terminal representation is still the entire isometric copy.

lemma OAI.WeakPureInfiniteness.exists_lipschitz_joined_unitary_path line 24
Source documentation
A connected unitary has some finite Lipschitz path, by its finite self-adjoint exponential decomposition. No uniform bound is asserted here.
```
lemma exists_lipschitz_joined_unitary_path (u : unitary E)
    (hu : Joined (1 : unitary E) u) :
    ∃ (L : ℝ), 0 ≤ L ∧ ∃ p : Path (1 : unitary E) u,
      ∀ a b, ‖(p a : E) - p b‖ ≤ L * |(a : ℝ) - b| := by
…
```
lemma OAI.WeakPureInfiniteness.binaryCornerUnitary_fixes line 53

lemma OAI.WeakPureInfiniteness.exists_uniform_binaryCorner_path line 63

Source documentation

The compressed unitary has a uniform path once a genuine unit-isometry in its fixed corner is supplied.

lemma exists_uniform_binaryCorner_path [Nontrivial E]
    (s : ℕ → E) (hs : ∀ i j, star (s i) * s j = if i = j then 1 else 0)
    (w z : E) (hw : star w * w = 1) (hz : star z * z = 1)
    (hswz : star w * z = 0) (u : unitary E) (hu : Joined (1 : unitary E) u) :
    ∃ p : Path (1 : unitary E) (binaryCornerUnitary w hw u),
      ∀ a b, ‖(p a : E) - p b‖ ≤ (9 * Real.pi) * |(a : ℝ) - b| := by
…

Mentions: OAI.WeakPureInfiniteness.binaryCornerUnitary

def OAI.WeakPureInfiniteness.bufferedIterationUnitary line 79
Source documentation
The actual unitary recursion used in buffered absorption.
```
def bufferedIterationUnitary (w : E) (hw : star w * w = 1)
    (u : unitary E) : ℕ → unitary E
  | 0 => 1
  | n + 1 => binaryCornerUnitary w hw (bufferedIterationUnitary w hw u n) * u
```
Mentions: OAI.WeakPureInfiniteness.binaryCornerUnitary
lemma OAI.WeakPureInfiniteness.bufferedIterationUnitary_joined line 84

lemma OAI.WeakPureInfiniteness.exists_uniform_bufferedIteration_paths line 95

Source documentation

Only the base path cost appears beside 9π; the iteration depth does not enter the bound. This statement does not bound that base cost uniformly.

lemma exists_uniform_bufferedIteration_paths [Nontrivial E]
    (s : ℕ → E) (hs : ∀ i j, star (s i) * s j = if i = j then 1 else 0)
    (w z : E) (hw : star w * w = 1) (hz : star z * z = 1)
    (hswz : star w * z = 0) (u : unitary E)
    (L : ℝ) (hL : 0 ≤ L) (p : Path (1 : unitary E) u)
    (hp : ∀ a b, ‖(p a : E) - p b‖ ≤ L * |(a : ℝ) - b|) :
    ∀ n, ∃ q : Path (1 : unitary E) (bufferedIterationUnitary w hw u n),
      ∀ a b, ‖(q a : E) - q b‖ ≤ (9 * Real.pi + L) * |(a : ℝ) - b| := by
…

Mentions: OAI.WeakPureInfiniteness.bufferedIterationUnitary

lemma OAI.WeakPureInfiniteness.bufferedIterationUnitary_error line 121

Source documentation

The exact residual formula and accumulated error for the concrete recursion whose paths were constructed above.

lemma bufferedIterationUnitary_error {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) (ε : ℝ)
    (he : ∀ i, ‖(u : E) * s i * star (u : E) -
      bufferedAbsorptionValue w (t i) (s i) 1‖ ≤ ε) (n : ℕ) :
    ∀ i, ‖(bufferedIterationUnitary w hw u n : E) * s i *
        star (bufferedIterationUnitary w hw u n : E) -
      bufferedAbsorptionValue w (t i) (s i) n‖ ≤ n * ε := by
…

Mentions: OAI.WeakPureInfiniteness.bufferedAbsorptionValue, OAI.WeakPureInfiniteness.bufferedIterationUnitary

lemma OAI.WeakPureInfiniteness.exists_canonical_buffered_path_iterations line 192

Source documentation

For each fixed one-step accuracy the canonical construction has one path bound for all depths. The accumulated error is exactly retained as m * η; choosing a new accuracy may also change the base path bound.

lemma exists_canonical_buffered_path_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‖ < κ) ∧
      ∀ η : ℝ, 0 < η → ∃ L : ℝ, 0 ≤ L ∧ ∀ m : ℕ,
        ∃ v : unitary E,
          (∀ i : Fin n, ‖(v : E) * s i * star (v : E) -
…

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