ClockCorrection.lean`

20 declarations, 0 contain sorry, 0 declared as axioms

Finite clock corrections and their multiplication defects

Clock powers remove the finite homogeneous degrees. They are not treated as central: every multiplication defect is an explicit commutator. Terms of degree divisible by the clock period are preserved exactly. The final formula applies this correction to the actual three-term cancellation path and preserves both endpoint values.

def OAI.WeakPureInfiniteness.clockDegreeCorrection line 22
Source documentation
Left correction of an integer homogeneous degree by a unitary clock.
```
def clockDegreeCorrection (k : unitary E) (d : ℤ) (x : E) : E :=
…
```
lemma OAI.WeakPureInfiniteness.clockDegreeCorrection_norm line 25
lemma OAI.WeakPureInfiniteness.clockDegreeCorrection_zero line 29
lemma OAI.WeakPureInfiniteness.clockDegreeCorrection_period line 33

lemma OAI.WeakPureInfiniteness.clockDegreeCorrection_mul_defect line 42

Source documentation

No centrality is suppressed in this identity.

lemma clockDegreeCorrection_mul_defect (k : unitary E) (d e : ℤ) (x y : E) :
    clockDegreeCorrection k d x * clockDegreeCorrection k e y -
      clockDegreeCorrection k (d + e) (x * y) =
        ((k ^ (-d) : unitary E) : E) *
          (x * ((k ^ (-e) : unitary E) : E) - ((k ^ (-e) : unitary E) : E) * x) * y := by
…

Mentions: OAI.WeakPureInfiniteness.clockDegreeCorrection

lemma OAI.WeakPureInfiniteness.clockDegreeCorrection_mul_error line 54
lemma OAI.WeakPureInfiniteness.clockDegreeCorrection_mul_of_commute line 61
lemma OAI.WeakPureInfiniteness.clockDegreeCorrection_star_defect line 68
lemma OAI.WeakPureInfiniteness.clockDegreeCorrection_add line 76
lemma OAI.WeakPureInfiniteness.clockDegreeCorrection_smul line 81
lemma OAI.WeakPureInfiniteness.clock_commutator_inverse line 85
lemma OAI.WeakPureInfiniteness.clock_commutator_pow line 101
lemma OAI.WeakPureInfiniteness.clock_commutator_zpow line 125
lemma OAI.WeakPureInfiniteness.clockDegreeCorrection_mul_error_of_commutator line 138

lemma OAI.WeakPureInfiniteness.clockDegreeCorrection_sum_product_error line 151

Source documentation

The full finite product estimate, with the actual pairwise commutators.

lemma clockDegreeCorrection_sum_product_error
    {I J : Type*} [Fintype I] [Fintype J]
    (k : unitary E) (d : I → ℤ) (e : J → ℤ) (x : I → E) (y : J → E) :
    ‖(∑ i, clockDegreeCorrection k (d i) (x i)) *
        (∑ j, clockDegreeCorrection k (e j) (y j)) -
      ∑ i, ∑ j, clockDegreeCorrection k (d i + e j) (x i * y j)‖ ≤
      ∑ i, ∑ j,
        ‖x i * ((k ^ (-e j) : unitary E) : E) -
          ((k ^ (-e j) : unitary E) : E) * x i‖ * ‖y j‖ := by
…

Mentions: OAI.WeakPureInfiniteness.clockDegreeCorrection

def OAI.WeakPureInfiniteness.clockCorrectedCancellation line 178
Source documentation
The explicit correction of the degree 0,1,-1 cancellation formula.
```
def clockCorrectedCancellation (k : unitary E) (a b u : E) (θ : ℝ) : E :=
…
```
lemma OAI.WeakPureInfiniteness.clockCorrectedCancellation_zero line 185
lemma OAI.WeakPureInfiniteness.clockCorrectedCancellation_pi_div_two line 193
lemma OAI.WeakPureInfiniteness.clockCorrectedCancellation_continuous line 198

lemma OAI.WeakPureInfiniteness.clockCorrectedCancellation_sub_bound line 205

Source documentation

At every angle the alteration is exactly the two degree corrections; this bound does not treat the clock as central.

lemma clockCorrectedCancellation_sub_bound (k : unitary E) (a b u : E)
    (ha : star a * a = 1) (hb : star b * b = 1)
    (hab : star a * b = 0) (hu : u * star u = 1) (θ : ℝ) :
    ‖clockCorrectedCancellation k a b u θ - cornerCancellationPath a b u θ‖ ≤
      |Real.sin θ * Real.cos θ| *
        (‖clockDegreeCorrection k 1 (a * (u - 1) * star b) - a * (u - 1) * star b‖ +
         ‖clockDegreeCorrection k (-1) (b * (star u - 1) * star a) -
            b * (star u - 1) * star a‖) := by
…

Mentions: OAI.WeakPureInfiniteness.clockCorrectedCancellation, OAI.WeakPureInfiniteness.cornerCancellationPath, OAI.WeakPureInfiniteness.clockDegreeCorrection