OAI/Probability/InvariantIsing/Fields/FieldSecondMeanDerivative.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The actual mixed derivative of one scalar Gaussian recursion step. The formula uses the affine-noise tangent, so it needs no third spatial derivative of the incoming scalar payoff.

  1. def OAI.InvariantIsing.FieldSecondFamily.mixedMean line 18
  2. lemma OAI.InvariantIsing.FieldSecondFamily.measurable_shiftedMean line 25
  3. lemma OAI.InvariantIsing.FieldSecondFamily.measurable_shiftedTangent line 28
  4. lemma OAI.InvariantIsing.FieldSecondFamily.measurable_shiftedMixed line 32
  5. lemma OAI.InvariantIsing.FieldSecondFamily.mean_hasFDerivAt line 36