OAI/Probability/InvariantIsing/Magnetic/MagneticFourJet.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

One additional bounded spatial derivative, exactly as needed to differentiate the inverse-coordinate curvature equation.

  1. structure OAI.InvariantIsing.MagneticContinuationFourJet line 14
  2. def OAI.InvariantIsing.MagneticContinuationFourJet.slope line 22
  3. def OAI.InvariantIsing.MagneticContinuationFourJet.square line 39
  4. def OAI.InvariantIsing.MagneticContinuationFourJet.transitionFourth line 58
  5. lemma OAI.InvariantIsing.MagneticContinuationFourJet.transition_third_eq line 68
  6. lemma OAI.InvariantIsing.MagneticContinuationFourJet.transitionFourth_measurable line 79
  7. lemma OAI.InvariantIsing.MagneticContinuationFourJet.transitionFourth_bounded line 91
  8. lemma OAI.InvariantIsing.MagneticContinuationFourJet.transition_hasDerivAt_third line 105
  9. def OAI.InvariantIsing.MagneticContinuationFourJet.transition line 123