OAI/Probability/InvariantIsing/Magnetic/RestrictedTreeRegular.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.restricted_tree_regular line 13