OAI/Probability/InvariantIsing/Fields/FieldSecondMeanBounds.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Uniform second-derivative bounds on a positive-variance interval. The constants depend on the interval bounds but not on the spatial bias.

  1. lemma OAI.InvariantIsing.affine_linear_integral_bound line 13
  2. def OAI.InvariantIsing.FieldSecondFamily.mixedMeanCap line 26
  3. def OAI.InvariantIsing.FieldSecondFamily.secondMeanCap line 30
  4. lemma OAI.InvariantIsing.FieldSecondFamily.mixedMean_bound line 36
  5. lemma OAI.InvariantIsing.FieldSecondFamily.secondMean_bound line 82