OAI/Probability/InvariantIsing/Magnetic/MagneticUniformSlabBounds.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Spatial bounds for the actual Gaussian transition, uniform in its variance. These are used to control both endpoints of inverse coordinates.

  1. def OAI.InvariantIsing.MagneticSlabBound line 14
  2. lemma OAI.InvariantIsing.MagneticSlabBound.const line 19
  3. lemma OAI.InvariantIsing.MagneticSlabBound.add line 22
  4. lemma OAI.InvariantIsing.MagneticSlabBound.sub line 29
  5. lemma OAI.InvariantIsing.MagneticSlabBound.mul line 36
  6. lemma OAI.InvariantIsing.MagneticSlabBound.transition line 44
  7. lemma OAI.InvariantIsing.MagneticSlabBound.spatial line 50
  8. lemma OAI.InvariantIsing.magneticContinuationSecond_uniform line 63
  9. lemma OAI.InvariantIsing.magneticContinuationThird_uniform line 77
  10. lemma OAI.InvariantIsing.MagneticContinuationJet.transition_second_uniform line 100
  11. lemma OAI.InvariantIsing.MagneticContinuationJet.transition_third_uniform line 106