OAI/Probability/InvariantIsing/Magnetic/MagneticContinuationTwoJet.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The variance generator requires only two derivatives of its bounded test. In particular it applies to the ordinary curvature without requiring a fifth derivative of the finite scalar field.

  1. structure OAI.InvariantIsing.MagneticContinuationTwoJet line 14
  2. def OAI.InvariantIsing.MagneticContinuationJet.toTwoJet line 27
  3. def OAI.InvariantIsing.MagneticContinuationJet.slopeTwoJet line 41