OAI/Probability/InvariantIsing/Fields/FieldGaussianFamilyGenerator.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The Gaussian generator with a varying, linearly growing scalar payoff. This is the covariance derivative used in the finite field chain.

  1. theorem OAI.InvariantIsing.field_gaussianFamily_hasFDerivAt line 14