OAI/Probability/InvariantIsing/Fields/FieldAffineAverageDerivative.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Applying the quadratic-envelope differentiation theorem to the actual affine Gaussian shift of a finite scalar-field family.

  1. def OAI.InvariantIsing.FieldSmoothFamily.affineShift line 18
  2. def OAI.InvariantIsing.FieldSmoothFamily.affineDifferential line 21
  3. lemma OAI.InvariantIsing.FieldSmoothFamily.affine_average_hasFDerivAt line 28