OAI/Probability/SLE/Gauge/MomentUnclipping.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Removing the prescribed integer clipping levels under the proved integrable terminal-moment bound.

  1. lemma OAI.SLEExactGauge.clip_nat_eventually_eq line 14
  2. lemma OAI.SLEExactGauge.weighted_clip_integral_bound line 21
  3. theorem OAI.SLEExactGauge.weighted_unclip_pow_tendsto line 43