OAI/Analysis/OInfinity/JordanWignerEstimates.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Quantitative stability of the finite Jordan–Wigner construction

The occupation parity is Lipschitz on normalized modes. Telescoping the finite parity prefixes gives the explicit (4k + 1)δ estimate, while scalar phases pass exactly through the construction. These estimates do not assert a unitary cocycle or a bound on its exponential length.

  1. lemma OAI.WeakPureInfiniteness.carNormalizedMode_norm_le_one line 20
  2. lemma OAI.WeakPureInfiniteness.carSelfAdjointSquare_norm_le_one line 25
  3. lemma OAI.WeakPureInfiniteness.carOccupation_sub_norm_le line 31
  4. lemma OAI.WeakPureInfiniteness.carModeParity_sub_norm_le line 44
  5. lemma OAI.WeakPureInfiniteness.carParityPrefix_norm_le_one line 54
  6. lemma OAI.WeakPureInfiniteness.carParityPrefix_sub_norm_le line 64
  7. lemma OAI.WeakPureInfiniteness.carJordanWigner_sub_norm_le line 94
  8. lemma OAI.WeakPureInfiniteness.carModeParity_smul line 120
  9. lemma OAI.WeakPureInfiniteness.carParityPrefix_smul line 128
  10. lemma OAI.WeakPureInfiniteness.carJordanWigner_smul line 138
  11. lemma OAI.WeakPureInfiniteness.evenRowShift_sub line 146
  12. lemma OAI.WeakPureInfiniteness.evenRowShift_carModeParity line 150
  13. lemma OAI.WeakPureInfiniteness.evenRowShift_carParityPrefix line 159
  14. lemma OAI.WeakPureInfiniteness.evenRowShift_carJordanWigner line 177
  15. lemma OAI.WeakPureInfiniteness.evenRowShift_normalizedMode line 190
  16. lemma OAI.WeakPureInfiniteness.evenRohlinCoordinate_shift_error line 210