OAI/Probability/InvariantIsing/Fields/FieldLogNormalizer.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The scalar field's actual logarithmic normalizer and its Gaussian recursion, including joint integrability in the root and forest.

  1. lemma OAI.InvariantIsing.field_energy_recursion line 15
  2. def OAI.InvariantIsing.fieldVectorLogNormalizer line 52
  3. lemma OAI.InvariantIsing.field_labeled_energy line 58
  4. lemma OAI.InvariantIsing.measurable_fieldVectorLogNormalizer line 68
  5. theorem OAI.InvariantIsing.field_vector_log_conditional line 85
  6. lemma OAI.InvariantIsing.field_vector_root_recursion_integrable line 136
  7. theorem OAI.InvariantIsing.field_vector_log_root_integral line 166