OAI/Probability/SLE/Geometry/FiniteLawTailBounds.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The batch estimates need only upper moment bounds on finite laws. Increasing finite-law tails can be passed to their supremum before summing.

  1. lemma OAI.SLEExactGauge.MomentBatches.upper_finite_batch_bound line 14
  2. lemma OAI.SLEExactGauge.MomentBatches.cleanup_finite_tail_bound line 39
  3. lemma OAI.SLEExactGauge.MomentBatches.finite_monotone_tail_sum_bound line 61