OAI/Probability/SLE/Mass/RadonKernelIntegral.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Signed integrals of a random Radon measure can be computed from its mean measure. The positive and negative parts use Tonelli separately.

  1. lemma OAI.SLEExactGauge.lintegral_ofReal_lt_top_of_integrable line 15
  2. theorem OAI.SLEExactGauge.integrable_integral_bind_of_sections line 22
  3. theorem OAI.SLEExactGauge.integral_bind_of_integrable_sections line 55