OAI/Analysis/OInfinity/EvenCARRelations.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

CAR relations for the actual finite even-row shift

The seed and parity are formed from the two equally sized blocks of the given row. Their iterates satisfy CAR and exact covariance on even products.

  1. lemma OAI.WeakPureInfiniteness.evenRowShift_smul line 22
  2. lemma OAI.WeakPureInfiniteness.evenRowShift_sum line 25
  3. lemma OAI.WeakPureInfiniteness.evenRowCAR_succ_commute_parity line 31
  4. lemma OAI.WeakPureInfiniteness.evenRowCAR_shift_single line 37
  5. lemma OAI.WeakPureInfiniteness.evenRowParity_shift_mul line 44
  6. lemma OAI.WeakPureInfiniteness.evenRowParity_shift_star_mul line 58
  7. lemma OAI.WeakPureInfiniteness.evenRowCAR_shift_even line 71
  8. lemma OAI.WeakPureInfiniteness.evenRowCAR_seed_anticommute line 98
  9. lemma OAI.WeakPureInfiniteness.evenRowCAR_anticommute line 115
  10. lemma OAI.WeakPureInfiniteness.evenRowCAR_seed_star_anticommute line 141
  11. lemma OAI.WeakPureInfiniteness.evenRowCAR_star_anticommute line 166
  12. lemma OAI.WeakPureInfiniteness.evenRowCAR_synthesis_norm_sq_le line 199