OAI/Probability/InvariantIsing/Magnetic/RestrictedFieldLogNormalizer.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The constrained block's actual logarithmic normalizer, with the original cube mass retained, equals its vector Gaussian recursion.

  1. lemma OAI.InvariantIsing.restricted_vector_recursion_const_add line 16
  2. lemma OAI.InvariantIsing.restricted_normalized_field_recursion line 36
  3. def OAI.InvariantIsing.restrictedFieldVectorLogNormalizer line 51
  4. lemma OAI.InvariantIsing.measurable_restrictedFieldVectorLogNormalizer line 57
  5. lemma OAI.InvariantIsing.restricted_normalized_root_integral line 64
  6. lemma OAI.InvariantIsing.integrable_restrictedFieldVectorLogNormalizer line 81
  7. theorem OAI.InvariantIsing.restricted_field_vector_log_root_integral line 89