OAI/Probability/SLE/Mass/WeightedImageRandomMass.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Measurable weighted images of locally finite random half-plane measures. The weight and image map can be chosen from the stopped past.

  1. def OAI.SLEExactGauge.weightedImageMass line 14
  2. lemma OAI.SLEExactGauge.weightedImageMass_apply line 19
  3. theorem OAI.SLEExactGauge.weightedImageMass_measurable line 27
  4. lemma OAI.SLEExactGauge.weightedImageMass_lintegral line 43
  5. theorem OAI.SLEExactGauge.weightedImageMass_measurable_of_subsigma line 52
  6. theorem OAI.SLEExactGauge.restart_weighted_mass_test line 66