OAI/Probability/InvariantIsing/Magnetic/RestrictedPhysicalCutoff.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Bounded cutoff tests for the actual perturbed Ising law, with the same Haar and Gaussian disorder in the full and restricted models.

  1. lemma OAI.InvariantIsing.restricted_cavity_full_exp_integrable_ae line 15
  2. def OAI.InvariantIsing.restrictedCavityFullCutoffDisorderTest line 34
  3. theorem OAI.InvariantIsing.restricted_cavity_full_cutoff_error line 43