OAI/Probability/SLE/Multipoint/MultipointLevelWeights.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

From the multipoint probability bound to the product estimate for actual stopped Green weights. The estimate is uniform in their levels.

  1. lemma OAI.SLEExactGauge.Multipoint.target_weight_capped line 15
  2. lemma OAI.SLEExactGauge.Multipoint.lintegral_ofReal_prod_le_event line 24
  3. lemma OAI.SLEExactGauge.Multipoint.stoppedGreen_level_bound line 41
  4. theorem OAI.SLEExactGauge.Multipoint.stoppedGreen_product_expectation_bound line 62