OAI/Probability/InvariantIsing/Cavity/CavityComparisonRates.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The dimension-dependent errors in the finite cavity comparison. The geometric cutoff is retained with its full Gaussian amplitude.

  1. def OAI.InvariantIsing.cavityWeightedKernel line 14
  2. lemma OAI.InvariantIsing.cavityWeightedKernel_split line 17
  3. lemma OAI.InvariantIsing.cavityWeightedKernel_abs_le line 22
  4. lemma OAI.InvariantIsing.cavityWeightedKernel_difference line 28
  5. theorem OAI.InvariantIsing.cavityWeightedKernel_amplitude_difference line 57
  6. def OAI.InvariantIsing.cavityCovarianceRate line 81
  7. lemma OAI.InvariantIsing.cavityCovarianceRate_nonneg line 86
  8. lemma OAI.InvariantIsing.cavityCovarianceRate_tendsto line 91