OAI/Probability/InvariantIsing/Cavity/ConsecutivePhysicalIncrement.lean

GitHub source file

4 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. lemma OAI.InvariantIsing.cavityBaseAmplitude_extend line 13
  2. def OAI.InvariantIsing.repeatedRotationIncrement line 21
  3. lemma OAI.InvariantIsing.consecutive_prior_increment_physical line 38
  4. lemma OAI.InvariantIsing.cavity_oriented_restricted_pressure line 66