OAI/Probability/InvariantIsing/Fields/FieldGaussianFamilyEnvelope.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A local exponential envelope for the two-parameter scalar Gaussian recursion. This is used with parameter and spatial coordinate together.

  1. lemma OAI.InvariantIsing.field_average_hasFDerivAt_of_envelope line 14