OAI/Probability/SLE/Multipoint/MultipointCenteredWeights.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A fixed additional approach event costs its target radius to the codimension power, uniformly in the levels of the integrated weights.

  1. lemma OAI.SLEExactGauge.Multipoint.lintegral_indicator_ofReal_prod_le_event line 14
  2. theorem OAI.SLEExactGauge.Multipoint.stoppedGreen_centered_product_expectation_bound line 36
  3. lemma OAI.SLEExactGauge.Multipoint.measurableSet_physical_radius_hit line 130
  4. theorem OAI.SLEExactGauge.Multipoint.stoppedGreen_centered_common_level_bound line 159