OAI/Probability/InvariantIsing/Cavity/CavityBoundaryCutoff.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Continuous upper and lower approximations to a hard radial cutoff.

  1. def OAI.InvariantIsing.cavityBoundaryUpper line 13
  2. def OAI.InvariantIsing.cavityBoundaryLower line 14
  3. def OAI.InvariantIsing.cavityBoundaryGap line 15
  4. lemma OAI.InvariantIsing.cavityBoundaryUpper_one line 17
  5. lemma OAI.InvariantIsing.cavityBoundaryLower_zero line 21
  6. lemma OAI.InvariantIsing.cavityBoundaryGap_mem line 27
  7. lemma OAI.InvariantIsing.cavityBoundaryUpper_error line 38
  8. lemma OAI.InvariantIsing.cavityBoundaryGap_tendsto line 49