OAI/Probability/InvariantIsing/Fields/PriorFieldLogNormalizer.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Logarithmic field normalizers for a deterministic finite spin prior, with joint root/forest integrability proved from the actual recursion.

  1. lemma OAI.InvariantIsing.prior_field_energy_recursion line 15
  2. def OAI.InvariantIsing.priorFieldVectorLogNormalizer line 51
  3. lemma OAI.InvariantIsing.measurable_priorFieldVectorLogNormalizer line 57
  4. theorem OAI.InvariantIsing.prior_field_vector_log_conditional line 74
  5. lemma OAI.InvariantIsing.prior_field_vector_root_recursion_integrable line 125
  6. theorem OAI.InvariantIsing.prior_field_vector_log_root_integral line 155
  7. theorem OAI.InvariantIsing.prior_field_vector_spin_exp_integrable line 179