OAI/Probability/InvariantIsing/Cavity/CavityCappedLogIntegrable.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The capped logarithm is integrable from the ordinary fourth moment. The moment need only hold almost surely in the disorder.

  1. lemma OAI.InvariantIsing.cavity_capped_log_integrable_ae line 14