OAI/Probability/InvariantIsing/Fields/FieldFiniteShiftData.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The joint gradient and Hessian of an affine-noise scalar payoff.

  1. lemma OAI.InvariantIsing.fieldFiniteLinear_add line 13
  2. lemma OAI.InvariantIsing.fieldFiniteLinear_smul line 21
  3. def OAI.InvariantIsing.FieldFiniteFamily.shiftPoint line 36
  4. def OAI.InvariantIsing.FieldFiniteFamily.shiftedMean line 39
  5. def OAI.InvariantIsing.FieldFiniteFamily.shiftedTangent line 42
  6. def OAI.InvariantIsing.FieldFiniteFamily.shiftedMixed line 45
  7. def OAI.InvariantIsing.FieldFiniteFamily.shiftedHessian line 48
  8. lemma OAI.InvariantIsing.FieldFiniteFamily.shiftedMean_hasFDerivAt line 55
  9. lemma OAI.InvariantIsing.FieldFiniteFamily.shiftedTangent_hasFDerivAt line 61
  10. lemma OAI.InvariantIsing.FieldFiniteFamily.shiftedHessian_symmetric line 80