OAI/Probability/InvariantIsing/Cavity/CavityFullTilt.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Identifying the two successive tilts with the full cavity factor on the original leaf/residual/spin prior, with the common root retained.

  1. def OAI.InvariantIsing.cavityRootedPriorKernel line 15
  2. instance OAI.InvariantIsing.cavityRootedPriorKernel_markov line 23
  3. def OAI.InvariantIsing.cavityRootedQuadratic line 28
  4. lemma OAI.InvariantIsing.measurable_cavityRootedQuadratic line 33
  5. lemma OAI.InvariantIsing.measurable_cavityRootedLogFactor line 38
  6. lemma OAI.InvariantIsing.cavity_residual_quadratic_integrable line 71
  7. theorem OAI.InvariantIsing.cavity_rooted_quadratic_eq_tilted line 89
  8. lemma OAI.InvariantIsing.cavity_tilt_prod_left line 113
  9. lemma OAI.InvariantIsing.cavityQuadratic_eq_inner line 124
  10. lemma OAI.InvariantIsing.cavity_rooted_exponent_split line 134
  11. lemma OAI.InvariantIsing.cavity_rooted_quadratic_integrable line 147
  12. theorem OAI.InvariantIsing.cavity_rooted_full_tilt_eq line 163
  13. theorem OAI.InvariantIsing.cavity_rooted_full_exp_integrable line 187