OAI/Probability/InvariantIsing/Fields/FieldRawTangent.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Gaussian integration by parts identifies the raw affine-noise tangent with the scalar variance generator already used in the field recursion.

  1. lemma OAI.InvariantIsing.fieldAmplitudeCurvature_abs_le line 13
  2. lemma OAI.InvariantIsing.FieldSecondFamily.rawTangent_eq line 29