OAI/Probability/SLE/Multipoint/MultipointPatternExpectation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Summing the conditional product estimate over the actual finite switch partition, then telescoping the downward product jumps.

  1. theorem OAI.SLEExactGauge.Multipoint.switchPattern_integral_le line 15
  2. theorem OAI.SLEExactGauge.Multipoint.finite_switched_product_expectation_le line 49