OAI/Probability/InvariantIsing/Magnetic/MagneticHeatCurvature.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The actual scalar curvature satisfies the differentiated heat equation. The computation uses only four derivatives of the finite scalar value.

  1. def OAI.InvariantIsing.magneticHeatCurvature line 14
  2. lemma OAI.InvariantIsing.magneticHeatCurvature_eq line 20
  3. theorem OAI.InvariantIsing.magneticHeatCurvature_hasFDerivAt line 30