OAI/Probability/SLE/Multipoint/MultipointTerminalProbability.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Convert the real-valued stopped product estimate into the successful event probability, after exhaustion by the concrete localizations.

  1. lemma OAI.SLEExactGauge.Multipoint.initial_phase_product_le_one line 14
  2. lemma OAI.SLEExactGauge.Multipoint.measure_le_of_eventual_real_products line 35
  3. theorem OAI.SLEExactGauge.Multipoint.measure_le_of_completed_phase_products line 51