OAI/Probability/InvariantIsing/Magnetic/RestrictedProductPrior.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Exact product decomposition for constrained cavity blocks. The normalization cost is the sum of the two original cube-mass costs.

  1. def OAI.InvariantIsing.cavityProductSlice line 15
  2. lemma OAI.InvariantIsing.mem_cavityProductSlice line 19
  3. lemma OAI.InvariantIsing.cavityProductSlice_card line 24
  4. lemma OAI.InvariantIsing.cavityProductSlice_nonempty line 28
  5. lemma OAI.InvariantIsing.cavityProductSlice_log_mass line 36
  6. theorem OAI.InvariantIsing.restricted_cavity_spin_split_prior line 44
  7. theorem OAI.InvariantIsing.restricted_cavity_spin_leaf_split_prior line 72