OAI/Probability/InvariantIsing/Cavity/CavityLogNormalizerTransport.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The full cavity logarithmic normalizer splits into the quadratic normalizer and the linear normalizer under the same innovation map.

  1. lemma OAI.InvariantIsing.cavity_log_integral_exp_add line 14
  2. def OAI.InvariantIsing.cavityRootedLogNormalizer line 26
  3. lemma OAI.InvariantIsing.measurable_cavityRootedLogNormalizer line 33
  4. lemma OAI.InvariantIsing.cavityRootedLogNormalizer_eq_residual line 44
  5. lemma OAI.InvariantIsing.cavity_residual_partition_toReal line 59
  6. theorem OAI.InvariantIsing.cavity_full_log_normalizer_transport line 81