OAI/Probability/InvariantIsing/Fields/FieldFiniteFamily.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Joint finite-height derivative data for the scalar Ising recursion. Only the covariance coordinates required by a finite subdivision occur.

  1. structure OAI.InvariantIsing.FieldFiniteFamily line 14
  2. def OAI.InvariantIsing.fieldFiniteLogCosh line 48
  3. lemma OAI.InvariantIsing.FieldFiniteFamily.spatial_derivative line 109
  4. lemma OAI.InvariantIsing.FieldFiniteFamily.spatial_mean_derivative line 116
  5. lemma OAI.InvariantIsing.FieldFiniteFamily.growth line 123
  6. def OAI.InvariantIsing.fieldFiniteVariance line 128
  7. def OAI.InvariantIsing.fieldFiniteSlope line 131
  8. def OAI.InvariantIsing.fieldFiniteCurvature line 134
  9. lemma OAI.InvariantIsing.fieldFiniteCurvature_symmetric line 137