OAI/Probability/InvariantIsing/Fields/FieldFiniteTransformBounds.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Uniform bounds on the joint gradient and Hessian after one Gaussian step, independent of the scalar spatial field.

  1. lemma OAI.InvariantIsing.FieldFiniteFamily.affine_bounded_integral_bound line 16
  2. lemma OAI.InvariantIsing.FieldFiniteFamily.bound_mean line 24
  3. lemma OAI.InvariantIsing.FieldFiniteFamily.bound_curvature line 28
  4. lemma OAI.InvariantIsing.FieldFiniteFamily.affine_linear_integral_bound line 49
  5. def OAI.InvariantIsing.FieldFiniteFamily.tangentCap line 58
  6. def OAI.InvariantIsing.FieldFiniteFamily.mixedMeanCap line 61
  7. def OAI.InvariantIsing.FieldFiniteFamily.secondMeanCap line 65
  8. lemma OAI.InvariantIsing.FieldFiniteFamily.bound_tangent line 70
  9. lemma OAI.InvariantIsing.FieldFiniteFamily.bound_mixedMean line 80
  10. lemma OAI.InvariantIsing.FieldFiniteFamily.bound_secondMean line 123