OAI/Probability/InvariantIsing/Magnetic/MagneticContinuationRegular.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Measurability and finite spatial derivative bounds for the actual Gaussian continuation formulas through order three.

  1. def OAI.InvariantIsing.MagneticContinuationBound line 14
  2. lemma OAI.InvariantIsing.MagneticContinuationBound.const line 19
  3. lemma OAI.InvariantIsing.MagneticContinuationBound.add line 22
  4. lemma OAI.InvariantIsing.MagneticContinuationBound.sub line 29
  5. lemma OAI.InvariantIsing.MagneticContinuationBound.mul line 36
  6. lemma OAI.InvariantIsing.MagneticContinuationBound.transition line 44
  7. lemma OAI.InvariantIsing.MagneticContinuationBound.spatial line 50
  8. lemma OAI.InvariantIsing.measurable_magneticContinuationSecond line 63
  9. lemma OAI.InvariantIsing.magneticContinuationSecond_bounded line 77
  10. lemma OAI.InvariantIsing.measurable_magneticContinuationThird line 91
  11. lemma OAI.InvariantIsing.magneticContinuationThird_bounded line 109