OAI/Probability/InvariantIsing/Magnetic/RestrictedFullTail.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Cutoff control in the full perturbed model. The bad compression event is paid for only by its probability, never by an inverse moment.

  1. lemma OAI.InvariantIsing.restrictedCavityFullDisorderTest_sub line 15
  2. lemma OAI.InvariantIsing.restrictedCavityFullDisorderTest_le_envelope line 45
  3. theorem OAI.InvariantIsing.restricted_full_radial_cutoff line 62
  4. theorem OAI.InvariantIsing.restricted_full_tail_probability line 144