OAI/Probability/InvariantIsing/Fields/FieldTiltedPairDerivative.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Covariance form of the derivative of an actual normalized average. This is the two-coordinate formula used by the finite scalar recursion.

  1. lemma OAI.InvariantIsing.field_tilted_integral_normalize line 14
  2. lemma OAI.InvariantIsing.field_tiltedFamily_covariance_hasFDerivAt line 27