OAI/Probability/InvariantIsing/Cavity/CavityFullCutoff.lean

GitHub source file

5 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. def OAI.InvariantIsing.cavityFullHamiltonian line 16
  2. lemma OAI.InvariantIsing.measurable_cavityFullHamiltonian line 22
  3. lemma OAI.InvariantIsing.cavity_full_exp_integrable_ae line 33
  4. def OAI.InvariantIsing.cavityFullCutoffDisorderTest line 52
  5. theorem OAI.InvariantIsing.cavity_full_cutoff_error line 61