OAI/Probability/SLE/Geometry/FiniteLawTailENN.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Summable dyadic and cleanup tails from increasing finite laws. No limiting probability measure or future-dependent density is required.

  1. lemma OAI.SLEExactGauge.MomentBatches.finite_probability_sum_eq line 14
  2. lemma OAI.SLEExactGauge.MomentBatches.upper_finite_batch_bound_enn line 25
  3. lemma OAI.SLEExactGauge.MomentBatches.limiting_upper_batch_bound line 35
  4. lemma OAI.SLEExactGauge.MomentBatches.limiting_cleanup_tail_bound line 54