OAI/Probability/SLE/Mass/RawMassPathLaw.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The raw mass has one measurable full-law event carrying all path properties simultaneously. Equal driver laws therefore preserve these properties without assuming measurability of an uncountable predicate.

  1. theorem OAI.SLEExactGauge.exists_raw_rational_radon_factor line 20
  2. lemma OAI.SLEExactGauge.rational_reconstruction_nonanticipating line 41
  3. theorem OAI.SLEExactGauge.raw_radon_path_properties_of_same_law line 55
  4. theorem OAI.SLEExactGauge.Multipoint.CanonicalMass.exists_raw_nonanticipating_with_good_set line 77