OAI/Probability/SLE/Gauge/CanonicalBatchFailure.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The exact prescribed batch has a nonempty chronological enumeration and enough total centered success probability. The finite failure estimate requires only the corresponding adapted half-probability inequalities.

  1. theorem OAI.SLEExactGauge.Multipoint.CanonicalMass.ordered_batch_success_budget line 26
  2. theorem OAI.SLEExactGauge.Multipoint.CanonicalMass.ordered_batch_failure_bound line 52