OAI/Probability/InvariantIsing/Fields/FieldSecondBounds.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Local bounds for the explicit first and second derivatives of the affine Gaussian mark in the finite scalar recursion.

  1. def OAI.InvariantIsing.FieldSecondFamily.shiftedMixed line 16
  2. def OAI.InvariantIsing.FieldSecondFamily.shiftedSecond line 21
  3. lemma OAI.InvariantIsing.FieldSecondFamily.shiftedTangent_bound line 30
  4. lemma OAI.InvariantIsing.FieldSecondFamily.shiftedMixed_bound line 46
  5. lemma OAI.InvariantIsing.FieldSecondFamily.shiftedSecond_bound line 62