OAI/Probability/SLE/Gauge/GaugeTailSum.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The prescribed gauge entries retain their multiplicities when tail probabilities are summed. Cleanup entries occur exactly once per batch.

  1. abbrev OAI.SLEExactGauge.Target.TailCode line 14
  2. def OAI.SLEExactGauge.Target.gaugeTailEquiv line 17
  3. lemma OAI.SLEExactGauge.Target.gauge_tail_sum_eq line 39