OAI/Probability/InvariantIsing/Cavity/CavityTreeRestrictedRegular.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Measurability and boundedness of the fixed-tree physical restricted mean needed to restore the random cascade prior.

  1. theorem OAI.InvariantIsing.cavity_restricted_tree_regular line 13