OAI/Probability/InvariantIsing/Fields/FieldFiniteTransformData.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The explicit joint gradient and Hessian of one finite-height Gaussian recursion step. All expressions use the same normalized Gaussian law.

  1. def OAI.InvariantIsing.FieldFiniteFamily.mean line 16
  2. def OAI.InvariantIsing.FieldFiniteFamily.tangent line 19
  3. def OAI.InvariantIsing.FieldFiniteFamily.curvature line 22
  4. def OAI.InvariantIsing.FieldFiniteFamily.mixedMean line 27
  5. def OAI.InvariantIsing.FieldFiniteFamily.secondMean line 32
  6. lemma OAI.InvariantIsing.FieldFiniteFamily.secondMean_symmetric line 37
  7. lemma OAI.InvariantIsing.FieldFiniteFamily.measurable_mean line 49
  8. lemma OAI.InvariantIsing.FieldFiniteFamily.measurable_tangent line 52
  9. lemma OAI.InvariantIsing.FieldFiniteFamily.measurable_curvature line 56
  10. lemma OAI.InvariantIsing.FieldFiniteFamily.measurable_mixedMean line 63
  11. lemma OAI.InvariantIsing.FieldFiniteFamily.measurable_secondMean line 70