OAI/Analysis/OInfinity/RohlinShift.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Quantitative cyclic partitions for the finite even-row shift

The exact dyadic projection partition is approximately cycled by the actual row endomorphism, with an explicit error tending to zero as the geometric blocks lengthen. No centrality for additional elements or cocycle unitary is asserted here.

  1. lemma OAI.WeakPureInfiniteness.carSpinProjection_sub_norm_le line 20
  2. lemma OAI.WeakPureInfiniteness.carSpinProjection_smul line 35
  3. lemma OAI.WeakPureInfiniteness.evenRowShift_carSpinProjection line 40
  4. lemma OAI.WeakPureInfiniteness.evenRowShift_isStarProjection line 48
  5. lemma OAI.WeakPureInfiniteness.evenRohlin_factor_shift_error line 64
  6. lemma OAI.WeakPureInfiniteness.evenRohlin_factor_properties line 75
  7. lemma OAI.WeakPureInfiniteness.evenRohlinProjection_shift_error line 85
  8. lemma OAI.WeakPureInfiniteness.evenRohlinProjection_period line 125
  9. lemma OAI.WeakPureInfiniteness.evenRohlinProjection_cyclic_error line 130
  10. lemma OAI.WeakPureInfiniteness.exists_evenRohlin_cyclic_partition line 145