ControlledAbsorption.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Controlled paths for the concrete absorption unitary

The two-swap Fock completion has its actual 4π path. The absorption polynomial is 2-Lipschitz on unitaries. Consequently its path bound depends on the fixed anchor, independently of the requested Fock error.

lemma OAI.WeakPureInfiniteness.BufferAbsorptionCorner.rotation_sub_norm_le line 20
lemma OAI.WeakPureInfiniteness.BufferAbsorptionCorner.absorption_sub_norm_le line 44

lemma OAI.WeakPureInfiniteness.BufferAbsorptionCorner.controlled_absorption_path line 66

Source documentation

Multiply the fixed anchor path by the normalized absorption path.

lemma BufferAbsorptionCorner.controlled_absorption_path [Nontrivial E]
    (D : BufferAbsorptionCorner E) (L K : ℝ)
    (p₀ : Path (1 : unitary E) D.anchor)
    (hp₀ : ∀ a b, ‖(p₀ a : E) - p₀ b‖ ≤ L * |(a : ℝ) - b|)
    (u : unitary E) (p : Path (1 : unitary E) u)
    (hp : ∀ a b, ‖(p a : E) - p b‖ ≤ K * |(a : ℝ) - b|) :
    ∃ q : Path (1 : unitary E) (D.absorption u),
      ∀ a b, ‖(q a : E) - q b‖ ≤ (L + 2 * K) * |(a : ℝ) - b| := by
…

Mentions: OAI.WeakPureInfiniteness.BufferAbsorptionCorner

lemma OAI.WeakPureInfiniteness.BufferAbsorptionCorner.exists_controlled_vacuum_absorption_on line 98

Source documentation

The actual Fock completion gives a path cost independent of its accuracy.

lemma BufferAbsorptionCorner.exists_controlled_vacuum_absorption_on [Nontrivial E]
    (D : BufferAbsorptionCorner E) (s t : I → E) (r z : 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)
    (hzz : star z * z = 1) (hqz : D.q * z = 0)
    (hzr : star z * r = 0) (hzs : ∀ i, star z * s i = 0)
    (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))
    (L : ℝ) (p₀ : Path (1 : unitary E) D.anchor)
    (hp₀ : ∀ a b, ‖(p₀ a : E) - p₀ b‖ ≤ L * |(a : ℝ) - b|)
…

Mentions: OAI.WeakPureInfiniteness.BufferAbsorptionCorner

lemma OAI.WeakPureInfiniteness.BufferAbsorptionCorner.exists_controlled_proper_vacuum_absorption line 167

Source documentation

The selected proper target row inherits the same accuracy-independent bound.

lemma BufferAbsorptionCorner.exists_controlled_proper_vacuum_absorption [Nontrivial E]
    (D : BufferAbsorptionCorner 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)
    (n : ℕ) (hqz : D.q * s (n + 2) = 0)
    (hqt : ∀ i, Commute D.q (t i))
    (hat : ∀ i, Commute (star D.a) (t i))
    (hbt : ∀ i, Commute (star D.b) (t i))
    (L : ℝ) (p₀ : Path (1 : unitary E) D.anchor)
    (hp₀ : ∀ a b, ‖(p₀ a : E) - p₀ b‖ ≤ L * |(a : ℝ) - b|)
    (ε : ℝ) (hε : 0 < ε) :
    ∃ U : unitary E,
…

Mentions: OAI.WeakPureInfiniteness.BufferAbsorptionCorner

lemma OAI.WeakPureInfiniteness.exists_canonical_uniform_buffered_paths line 271

Source documentation

The concrete canonical corner has a single path bound for every depth and every requested final error. The exact terminal representation remains in the target of the estimate.

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

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