OAI/Analysis/OInfinity/DyadicProjections.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

Finite dyadic phase projections

The commuting two-level coordinates give exact finite partitions of the corner unit. The phase conditions are the elementary dyadic root identities; the shift estimates and cocycle construction are separate obligations.

  1. def OAI.WeakPureInfiniteness.carSpinAxis line 19
  2. def OAI.WeakPureInfiniteness.carSpinProjection line 21
  3. lemma OAI.WeakPureInfiniteness.carSpinAxis_star line 23
  4. lemma OAI.WeakPureInfiniteness.carSpinAxis_support line 26
  5. lemma OAI.WeakPureInfiniteness.carSpinAxis_sq line 37
  6. lemma OAI.WeakPureInfiniteness.carSpinProjection_support line 49
  7. lemma OAI.WeakPureInfiniteness.carSpinProjection_isStarProjection line 58
  8. lemma OAI.WeakPureInfiniteness.carSpinAxis_neg line 77
  9. lemma OAI.WeakPureInfiniteness.carSpinProjection_neg line 80
  10. lemma OAI.WeakPureInfiniteness.carSpinProjection_opposite_mul line 91
  11. lemma OAI.WeakPureInfiniteness.carSpinAxis_commute line 101
  12. lemma OAI.WeakPureInfiniteness.carSpinProjection_commute line 110
  13. def OAI.WeakPureInfiniteness.dyadicSpinProjection line 127

    Source documentation

    Ordered finite product, starting at the corner unit.

    def dyadicSpinProjection (q : E) (a : ℕ → E) (ζ : ℕ → ℂ) : ℕ → ℕ → E
  | 0, _ => q
  | m + 1, k => dyadicSpinProjection q a ζ m k * carSpinProjection q (a m) (ζ m ^ k)

section Dyadic

variable (q : E) (a : ℕ → E) (ζ : ℕ → ℂ)
  (hqstar : star q = q) (hqq : q * q = q)
  (hleft : ∀ i, q * a i = a i) (hright : ∀ i, a i * q = a i)
  (hzero : ∀ i, a i * a i = 0)
  (hgram : ∀ i, star (a i) * a i + a i * star (a i) = q)
  (hcomm : ∀ i j, Commute (a i) (a j))
…

    Mentions: OAI.WeakPureInfiniteness.carSpinProjection

  14. lemma OAI.WeakPureInfiniteness.dyadicSpinProjection_support line 144
  15. lemma OAI.WeakPureInfiniteness.dyadicSpinProjection_commute_factor line 160
  16. lemma OAI.WeakPureInfiniteness.dyadicSpinProjection_isStarProjection line 173
  17. lemma OAI.WeakPureInfiniteness.dyadic_phase_period line 185
  18. lemma OAI.WeakPureInfiniteness.dyadicSpinProjection_eq_of_phases line 197
  19. lemma OAI.WeakPureInfiniteness.dyadicSpinProjection_period line 208
  20. lemma OAI.WeakPureInfiniteness.dyadicSpinProjection_upper_half line 215
  21. lemma OAI.WeakPureInfiniteness.dyadicSpinProjection_split line 224
  22. lemma OAI.WeakPureInfiniteness.dyadicSpinProjection_sum line 236
  23. lemma OAI.WeakPureInfiniteness.dyadicSpinProjection_next_mul_eq_zero line 246
  24. lemma OAI.WeakPureInfiniteness.dyadicSpinProjection_opposite_children line 264
  25. lemma OAI.WeakPureInfiniteness.dyadicSpinProjection_orthogonal line 286