OAI/Probability/InvariantIsing/Magnetic/MagneticWeightedJet.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Spatial derivatives of q²Hᵤᵤ. Multiplying by q² removes the first-order term from the differentiated inverse-coordinate continuation equation.

  1. def OAI.InvariantIsing.magneticWeightedJetValue line 13
  2. def OAI.InvariantIsing.magneticWeightedJetFirst line 16
  3. def OAI.InvariantIsing.magneticWeightedJetSecond line 20
  4. lemma OAI.InvariantIsing.magneticWeightedJetValue_hasDerivAt line 28
  5. lemma OAI.InvariantIsing.magneticWeightedJetFirst_hasDerivAt line 39
  6. def OAI.InvariantIsing.magneticWeightedInverseSecond line 53
  7. lemma OAI.InvariantIsing.magneticWeightedInverseFirst_hasDerivAt line 57
  8. lemma OAI.InvariantIsing.magneticWeighted_forward_generator line 65