OAI/Analysis/OInfinity/CARShiftModes.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

Finite geometric modes for the binary corner shift

A normalized geometric block has a shift error at its two endpoints only. The squared coefficient error is exactly 2 / L; the CAR norm estimate transfers it to actual elements of the C*-algebra. Blocks whose index intervals are disjoint have zero mixed anticommutator. The shift here is x ↦ a*x*star a + b*x*star b for a relative Cuntz pair.

  1. def OAI.WeakPureInfiniteness.carModeScale line 19
  2. def OAI.WeakPureInfiniteness.carModeCoefficient line 21
  3. lemma OAI.WeakPureInfiniteness.carModeScale_nonneg line 24
  4. lemma OAI.WeakPureInfiniteness.carModeScale_normalized line 27
  5. lemma OAI.WeakPureInfiniteness.carModeScale_sq line 36
  6. lemma OAI.WeakPureInfiniteness.carModeCoefficient_norm line 42
  7. lemma OAI.WeakPureInfiniteness.carModeCoefficient_step line 47
  8. lemma OAI.WeakPureInfiniteness.carModeCoefficient_norm_sq_sum line 57
  9. lemma OAI.WeakPureInfiniteness.carModeCoefficient_inner_self line 64
  10. def OAI.WeakPureInfiniteness.carModeInitialCoefficient line 79
  11. def OAI.WeakPureInfiniteness.carModeShiftCoefficient line 82
  12. lemma OAI.WeakPureInfiniteness.carModeCoefficient_endpoint_error line 85
  13. lemma OAI.WeakPureInfiniteness.carModeCoefficient_error_sq_sum line 106

    Source documentation

    The error has two coefficients of equal modulus, with no interior contribution.

    lemma carModeCoefficient_error_sq_sum (L : ℕ) (hL : 0 < L)
    (ζ : ℂ) (hζ : ‖ζ‖ = 1) :
    (∑ i : Fin (L + 1),
      ‖carModeShiftCoefficient L ζ i - ζ * carModeInitialCoefficient L ζ i‖ ^ 2) =
      2 / (L : ℝ) := by
…

    Mentions: OAI.WeakPureInfiniteness.carModeShiftCoefficient, OAI.WeakPureInfiniteness.carModeInitialCoefficient

  14. lemma OAI.WeakPureInfiniteness.carSynthesis_cross_mul line 147
  15. lemma OAI.WeakPureInfiniteness.carSynthesis_cross_anticommute line 159
  16. def OAI.WeakPureInfiniteness.carGeometricMode line 175
  17. def OAI.WeakPureInfiniteness.carGeometricShift line 179
  18. lemma OAI.WeakPureInfiniteness.carGeometricMode_as_synthesis line 183
  19. lemma OAI.WeakPureInfiniteness.carGeometricShift_as_synthesis line 192
  20. lemma OAI.WeakPureInfiniteness.carGeometricMode_gram line 208
  21. lemma OAI.WeakPureInfiniteness.carGeometricMode_norm_le_one line 230
  22. lemma OAI.WeakPureInfiniteness.carGeometricMode_anticommute line 244
  23. lemma OAI.WeakPureInfiniteness.carGeometricMode_disjoint_star_anticommute line 252
  24. lemma OAI.WeakPureInfiniteness.carGeometricMode_shift_error line 269
  25. lemma OAI.WeakPureInfiniteness.zeroCornerCAR_shift_single line 293
  26. lemma OAI.WeakPureInfiniteness.carGeometricMode_shift line 302
  27. lemma OAI.WeakPureInfiniteness.zeroCornerParity_norm_le_one line 314
  28. lemma OAI.WeakPureInfiniteness.carGeometricMode_twisted_shift_error line 325