OAI/Probability/SLE/Multipoint/MultipointIntegratedCost.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Integrating finitely many active-interval costs. The interval endpoints may be different for every point or pair.

  1. lemma OAI.SLEExactGauge.Multipoint.active_interval_integral line 13
  2. lemma OAI.SLEExactGauge.Multipoint.active_interval_integrable line 22
  3. theorem OAI.SLEExactGauge.Multipoint.finite_active_cost_integral_le line 27
  4. theorem OAI.SLEExactGauge.Multipoint.dominated_active_cost_integral_le line 41