OAI/Probability/InvariantIsing/Fields/FieldAdjacentDerivative.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The adjacent-variance cancellation for a single field height. Its derivative is the negative conditional squared spin mean. This proves the local identity underlying fld:backward-derivative directly from the Gaussian recursion.

  1. theorem OAI.InvariantIsing.FieldSmoothFamily.parameter_derivative line 15
  2. theorem OAI.InvariantIsing.FieldSmoothFamily.negative_variance_compensation line 23
  3. theorem OAI.InvariantIsing.FieldSmoothFamily.adjacent_tangent line 41