OAI/Probability/InvariantIsing/Fields/FieldFiniteTransformDerivative.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Joint first and second derivatives of the actual finite-height Gaussian step, with the Hessian expressed by the tilted covariance.

  1. lemma OAI.InvariantIsing.FieldFiniteFamily.value_coordinate_derivative line 16
  2. lemma OAI.InvariantIsing.FieldFiniteFamily.mean_hasFDerivAt line 40
  3. lemma OAI.InvariantIsing.FieldFiniteFamily.tangent_hasFDerivAt line 77