OAI/Analysis/OInfinity/EvenShiftModes.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

Geometric modes for a finite even-row shift

The coefficient calculation is shared with the binary case, but the CAR family and shift here come from the actual given finite even row.

  1. def OAI.WeakPureInfiniteness.evenGeometricMode line 18
  2. def OAI.WeakPureInfiniteness.evenGeometricShift line 22
  3. lemma OAI.WeakPureInfiniteness.evenGeometricShift_eq line 26
  4. lemma OAI.WeakPureInfiniteness.evenGeometricMode_as_synthesis line 36
  5. lemma OAI.WeakPureInfiniteness.evenGeometricShift_as_synthesis line 45
  6. lemma OAI.WeakPureInfiniteness.evenGeometricMode_support line 60
  7. lemma OAI.WeakPureInfiniteness.evenGeometricMode_gram line 70
  8. lemma OAI.WeakPureInfiniteness.evenGeometricMode_square_zero line 90
  9. lemma OAI.WeakPureInfiniteness.evenGeometricMode_norm_le_one line 97
  10. lemma OAI.WeakPureInfiniteness.evenGeometricMode_shift_error line 111
  11. lemma OAI.WeakPureInfiniteness.evenGeometricMode_shift line 135
  12. lemma OAI.WeakPureInfiniteness.evenGeometricMode_commute_parity line 145
  13. lemma OAI.WeakPureInfiniteness.evenGeometricShift_commute_parity line 159
  14. lemma OAI.WeakPureInfiniteness.modeSymmetry_norm_le_one line 165
  15. def OAI.WeakPureInfiniteness.evenModeSymmetry line 180
  16. def OAI.WeakPureInfiniteness.evenShiftSymmetry line 183
  17. def OAI.WeakPureInfiniteness.evenEigenMode line 186
  18. lemma OAI.WeakPureInfiniteness.evenModeSymmetry_support line 190
  19. lemma OAI.WeakPureInfiniteness.evenShiftSymmetry_support line 199
  20. lemma OAI.WeakPureInfiniteness.evenShiftSymmetry_norm_le_one line 205
  21. lemma OAI.WeakPureInfiniteness.evenModeSymmetry_shift line 213
  22. lemma OAI.WeakPureInfiniteness.evenEigenMode_shift line 224
  23. lemma OAI.WeakPureInfiniteness.evenEigenMode_shift_error line 240