OAI/Probability/InvariantIsing/Fields/FieldGaussianFamilyRaw.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The raw two-coordinate derivative for a scalar Gaussian recursion with affine variance and a locally uniformly linearly growing payoff.

  1. theorem OAI.InvariantIsing.field_gaussianFamily_raw_hasFDerivAt line 15