OAI/Probability/InvariantIsing/Cavity/OffsetPhysicalIncrement.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The consecutive prior increment is the original physical constrained rotation increment, with the same base perturbation in both dimensions.

  1. def OAI.InvariantIsing.offsetRotationIncrement line 14
  2. lemma OAI.InvariantIsing.offset_prior_increment_physical line 32