OAI/Probability/InvariantIsing/Magnetic/RestrictedTreeLogIntegrability.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The canonical capped logarithm remains integrable after averaging an arbitrary finite cascade law and the independent compression data.

  1. lemma OAI.InvariantIsing.integrable_restricted_canonical_tree_log line 14