OAI/Probability/InvariantIsing/Cavity/CavityRadiusRemoval.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Removing the continuous radius cutoff from replica observables. The estimates also cover the convention at a zero cutoff normalizer.

  1. lemma OAI.InvariantIsing.cavity_radial_cutoff_moment_error line 14
  2. lemma OAI.InvariantIsing.cavity_soft_radius_replica_error line 34
  3. theorem OAI.InvariantIsing.cavity_soft_radius_mean_error line 48