OAI/Probability/InvariantIsing/Fields/FieldGaussianFamilyLocal.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The affine-variance generator needs no separate uniform-growth hypothesis: the bounded spatial derivative and joint differentiability produce it on a neighborhood of each positive-variance point.

  1. theorem OAI.InvariantIsing.field_gaussianFamily_local_hasFDerivAt line 15