OAI/Probability/InvariantIsing/Magnetic/MagneticWeightedSpatial.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Actual spatial derivatives and the uniformly bounded potential of the weighted inverse-coordinate continuation equation.

  1. lemma OAI.InvariantIsing.magneticScalarSlabFourJet_pos line 14
  2. lemma OAI.InvariantIsing.magneticScalarSlabBias_hasDerivAt_fourJet line 21
  3. def OAI.InvariantIsing.magneticScalarWeightedSlope line 29
  4. def OAI.InvariantIsing.magneticScalarWeightedSecond line 36
  5. lemma OAI.InvariantIsing.magneticScalarSlabWeighted_hasDerivAt_spin line 41
  6. lemma OAI.InvariantIsing.magneticScalarWeightedSlope_hasDerivAt_spin line 54
  7. lemma OAI.InvariantIsing.magneticScalarSlabWeighted_second_deriv line 63
  8. def OAI.InvariantIsing.magneticScalarWeightedPotential line 73
  9. lemma OAI.InvariantIsing.magneticScalarWeightedPotential_bound line 78
  10. lemma OAI.InvariantIsing.magneticScalarWeightedPotential_eq_fourJet line 97
  11. theorem OAI.InvariantIsing.magneticScalarSlabWeighted_PDE line 112