OAI/Probability/InvariantIsing/Fields/FieldFiniteRecursion.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Closure of the finite scalar Ising recursion under joint height and spatial derivatives. The Hessian symmetry is part of the constructed data.

  1. lemma OAI.InvariantIsing.FieldFiniteFamily.measurable_value line 16
  2. def OAI.InvariantIsing.FieldFiniteFamily.transform line 21
  3. structure OAI.InvariantIsing.FieldFiniteStep line 69
  4. def OAI.InvariantIsing.fieldFiniteValue line 74
  5. def OAI.InvariantIsing.fieldFiniteFamily line 79
  6. theorem OAI.InvariantIsing.fieldFiniteFamily_value line 97