OAI/Analysis/OInfinity/ClockGram.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Both Gram errors of the actual clock-corrected path

The homogeneous convolution identities follow from the two-isometry cancellation formula. The failure of the clock to commute with its three coefficients is retained quantitatively. Both Gram errors are controlled; neither invertibility nor unitarity is assumed.

  1. lemma OAI.WeakPureInfiniteness.clock_commutator_star line 20
  2. lemma OAI.WeakPureInfiniteness.clockDegreeCorrection_star_error line 33
  3. lemma OAI.WeakPureInfiniteness.clock_three_sum_norm line 39
  4. lemma OAI.WeakPureInfiniteness.clock_three_sum_star_error line 48
  5. lemma OAI.WeakPureInfiniteness.clock_three_sum_product_error line 66
  6. lemma OAI.WeakPureInfiniteness.clock_three_initial_gram_error line 93

    Source documentation

    Exact convolution and small coefficient commutators bound the initial Gram error. The cardinality here is exactly the three terms used above.

    lemma clock_three_initial_gram_error (k : unitary E)
    (d : Fin 3 → ℤ) (x : Fin 3 → E) (δ M : ℝ)
    (hδ : 0 ≤ δ) (_hM : 0 ≤ M) (hd : ∀ i, (d i).natAbs ≤ 1)
    (hc : ∀ i, ‖x i * (k : E) - (k : E) * x i‖ ≤ δ)
    (hx : ∀ i, ‖x i‖ ≤ M)
    (hg : (∑ i, ∑ j, clockDegreeCorrection k (-d i + d j) (star (x i) * x j)) = 1) :
    ‖star (∑ i, clockDegreeCorrection k (d i) (x i)) *
      (∑ i, clockDegreeCorrection k (d i) (x i)) - 1‖ ≤ 18 * M * δ := by
…

    Mentions: OAI.WeakPureInfiniteness.clockDegreeCorrection

  7. lemma OAI.WeakPureInfiniteness.clock_three_final_gram_error line 120

    Source documentation

    The same argument controls the final Gram error independently.

    lemma clock_three_final_gram_error (k : unitary E)
    (d : Fin 3 → ℤ) (x : Fin 3 → E) (δ M : ℝ)
    (hδ : 0 ≤ δ) (hM : 0 ≤ M) (hd : ∀ i, (d i).natAbs ≤ 1)
    (hc : ∀ i, ‖x i * (k : E) - (k : E) * x i‖ ≤ δ)
    (hx : ∀ i, ‖x i‖ ≤ M)
    (hg : (∑ i, ∑ j, clockDegreeCorrection k (d i - d j) (x i * star (x j))) = 1) :
    ‖(∑ i, clockDegreeCorrection k (d i) (x i)) *
      star (∑ i, clockDegreeCorrection k (d i) (x i)) - 1‖ ≤ 18 * M * δ := by
…

    Mentions: OAI.WeakPureInfiniteness.clockDegreeCorrection

  8. lemma OAI.WeakPureInfiniteness.clockCorrectedCancellation_gram_errors line 149

    Source documentation

    Both Gram errors for the actual corrected cancellation, with precisely the coefficient commutators still to be supplied by the chosen finite clock.

    lemma clockCorrectedCancellation_gram_errors (k : unitary E) (a b u : E)
    (ha : star a * a = 1) (hb : star b * b = 1) (hab : star a * b = 0)
    (hu : u ∈ unitary E) (θ δ M : ℝ) (hδ : 0 ≤ δ) (hM : 0 ≤ M)
    (hc : ∀ i, ‖clockCancellationCoefficients a b u θ i * (k : E) -
      (k : E) * clockCancellationCoefficients a b u θ i‖ ≤ δ)
    (hx : ∀ i, ‖clockCancellationCoefficients a b u θ i‖ ≤ M) :
    ‖star (clockCorrectedCancellation k a b u θ) *
        clockCorrectedCancellation k a b u θ - 1‖ ≤ 18 * M * δ ∧
    ‖clockCorrectedCancellation k a b u θ *
        star (clockCorrectedCancellation k a b u θ) - 1‖ ≤ 18 * M * δ := by
…

    Mentions: OAI.WeakPureInfiniteness.clockCancellationCoefficients, OAI.WeakPureInfiniteness.clockCorrectedCancellation

  9. lemma OAI.WeakPureInfiniteness.clock_isometry_norm line 167
  10. lemma OAI.WeakPureInfiniteness.clock_triple_norm line 173
  11. lemma OAI.WeakPureInfiniteness.clockCancellationCoefficients_norm_le line 183

    Source documentation

    All three actual coefficients have a uniform norm bound in the path parameter.

    lemma clockCancellationCoefficients_norm_le (a b u : E)
    (ha : star a * a = 1) (hb : star b * b = 1)
    (hu : u ∈ unitary E) (θ : ℝ) (i : Fin 3) :
    ‖clockCancellationCoefficients a b u θ i‖ ≤ 5 := by
…

    Mentions: OAI.WeakPureInfiniteness.clockCancellationCoefficients

  12. lemma OAI.WeakPureInfiniteness.clock_product_commutator line 228

    Distinct definitions of this name: OAI/Analysis/OInfinity/ClockFragmentation.lean:54 (different declaration text). Qualify references as OAI.WeakPureInfiniteness.clock_product_commutator@path.

  13. lemma OAI.WeakPureInfiniteness.clock_triple_commutator line 238
  14. lemma OAI.WeakPureInfiniteness.clockCancellationCoefficients_commutator_le line 262

    Source documentation

    The actual coefficients commute with the clock whenever the two supplied isometries and the supplied unitary do; the bound is uniform in the angle.

    lemma clockCancellationCoefficients_commutator_le (k : unitary E) (a b u : E)
    (ha : star a * a = 1) (hb : star b * b = 1) (hu : u ∈ unitary E)
    (δ : ℝ) (hδ : 0 ≤ δ)
    (hca : ‖a * (k : E) - (k : E) * a‖ ≤ δ)
    (hcb : ‖b * (k : E) - (k : E) * b‖ ≤ δ)
    (hcu : ‖u * (k : E) - (k : E) * u‖ ≤ δ) (θ : ℝ) (i : Fin 3) :
    ‖clockCancellationCoefficients a b u θ i * (k : E) -
      (k : E) * clockCancellationCoefficients a b u θ i‖ ≤ 10 * δ := by
…

    Mentions: OAI.WeakPureInfiniteness.clockCancellationCoefficients

  15. lemma OAI.WeakPureInfiniteness.clockCorrectedCancellation_gram_errors_of_constituents line 329

    Source documentation

    Uniform quantitative near-unitarity of the actual corrected path, from only its constituent commutators.

    lemma clockCorrectedCancellation_gram_errors_of_constituents (k : unitary E) (a b u : E)
    (ha : star a * a = 1) (hb : star b * b = 1) (hab : star a * b = 0)
    (hu : u ∈ unitary E) (δ : ℝ) (hδ : 0 ≤ δ)
    (hca : ‖a * (k : E) - (k : E) * a‖ ≤ δ)
    (hcb : ‖b * (k : E) - (k : E) * b‖ ≤ δ)
    (hcu : ‖u * (k : E) - (k : E) * u‖ ≤ δ) (θ : ℝ) :
    ‖star (clockCorrectedCancellation k a b u θ) *
        clockCorrectedCancellation k a b u θ - 1‖ ≤ 900 * δ ∧
    ‖clockCorrectedCancellation k a b u θ *
        star (clockCorrectedCancellation k a b u θ) - 1‖ ≤ 900 * δ := by
…

    Mentions: OAI.WeakPureInfiniteness.clockCorrectedCancellation