OAI/Probability/InvariantIsing/Fields/FieldScalarScaling.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Change of position units for the actual finite conditional spin chain. The spin observable acquires no multiplicative derivative factor.

  1. def OAI.InvariantIsing.fieldScaleIncrements line 15
  2. lemma OAI.InvariantIsing.fieldScaleIncrements_length line 18
  3. lemma OAI.InvariantIsing.scalar_value_measurable line 22
  4. lemma OAI.InvariantIsing.scalar_mean_measurable line 31
  5. lemma OAI.InvariantIsing.scalar_squares_measurable line 39
  6. lemma OAI.InvariantIsing.fieldSpinTransition_scale_position line 50
  7. lemma OAI.InvariantIsing.fieldScalarValue_scale_position line 66
  8. lemma OAI.InvariantIsing.fieldScalarMean_scale_position line 81
  9. lemma OAI.InvariantIsing.fieldScalarSquares_scale_position line 101
  10. lemma OAI.InvariantIsing.fieldScalarOverlaps_scale_position line 128