OAI/Probability/InvariantIsing/Magnetic/MagneticFieldGradient.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The exact physical height gradient at an arbitrary bias, and hence at the bias realizing a prescribed magnetization.

  1. lemma OAI.InvariantIsing.hasDerivAt_fieldInteriorChart_bias line 17
  2. lemma OAI.InvariantIsing.magnetic_terminal_list_zero line 26
  3. lemma OAI.InvariantIsing.hasDerivAt_fieldFinalChart_bias line 40
  4. lemma OAI.InvariantIsing.hasDerivAt_fieldHeightCoordinate_bias line 63
  5. lemma OAI.InvariantIsing.fieldFinite_centered_coordinate_derivative_bias line 81
  6. theorem OAI.InvariantIsing.magneticHeight_gradient_identification line 100
  7. lemma OAI.InvariantIsing.magneticHeight_optimized_gradient line 122