OAI/Probability/InvariantIsing/Cavity/CavitySoftCutoff.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Continuous cutoffs for finite-replica passage. Their removal costs only the discarded mass, including the zero-normalizer convention.

  1. lemma OAI.InvariantIsing.cavity_normalized_cutoff_algebra line 14
  2. theorem OAI.InvariantIsing.cavity_soft_cutoff_replica_error line 37
  3. def OAI.InvariantIsing.cavityRadialCutoff line 76
  4. lemma OAI.InvariantIsing.continuous_cavityRadialCutoff line 78
  5. lemma OAI.InvariantIsing.cavityRadialCutoff_mem line 82
  6. lemma OAI.InvariantIsing.cavityRadialCutoff_eq_one line 85
  7. lemma OAI.InvariantIsing.cavityRadialCutoff_eq_zero line 89
  8. lemma OAI.InvariantIsing.cavity_radial_cutoff_discarded_mass line 94