OAI/Analysis/OInfinity/CARCombination.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Finite linear combinations of the corner CAR generators

Only finite sums are used. The anticommutator gives the Euclidean coefficient bound directly, and the corner shift acts exactly on the required even products. No infinite CAR algebra or representation theorem is assumed.

  1. def OAI.WeakPureInfiniteness.carSynthesis line 20
  2. lemma OAI.WeakPureInfiniteness.carSynthesis_sub line 22
  3. lemma OAI.WeakPureInfiniteness.carSynthesis_star line 26
  4. lemma OAI.WeakPureInfiniteness.carSynthesis_mul line 30
  5. lemma OAI.WeakPureInfiniteness.carSynthesis_support line 41
  6. lemma OAI.WeakPureInfiniteness.carSynthesis_anticommute line 49
  7. lemma OAI.WeakPureInfiniteness.carSynthesis_square_zero line 64
  8. lemma OAI.WeakPureInfiniteness.carSynthesis_star_anticommute line 73
  9. lemma OAI.WeakPureInfiniteness.carSynthesis_norm_sq_le line 93
  10. lemma OAI.WeakPureInfiniteness.carSynthesis_norm_sub_sq_le line 112
  11. lemma OAI.WeakPureInfiniteness.zeroCornerShift_smul line 122
  12. lemma OAI.WeakPureInfiniteness.zeroCornerShift_sum line 126
  13. lemma OAI.WeakPureInfiniteness.zeroCornerCAR_synthesis_norm_sq_le line 137
  14. lemma OAI.WeakPureInfiniteness.zeroCornerCAR_synthesis_shift_even line 151
  15. lemma OAI.WeakPureInfiniteness.zeroCornerCAR_synthesis_shift_even_mul line 166