OAI/Probability/SLE/Multipoint/MultipointSuccess.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The terminal probability step for the multipoint product. Analytic estimates enter through the expected stopped product and its deterministic lower bound on success; completed points have already been frozen.

  1. lemma OAI.SLEExactGauge.Multipoint.measure_le_of_eventual_stopped_products line 15
  2. def OAI.SLEExactGauge.Multipoint.successBarrier line 34
  3. lemma OAI.SLEExactGauge.Multipoint.successBarrier_pos line 37
  4. lemma OAI.SLEExactGauge.Multipoint.successBarrier_inv line 40
  5. lemma OAI.SLEExactGauge.Multipoint.radius_target_exponential line 49
  6. lemma OAI.SLEExactGauge.Multipoint.radius_targets_exponential line 58