OAI/Probability/SLE/Mass/RawMassFunctional.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A fixed raw, nonanticipating mass functional on continuous driver paths. Each rational slice is first factored through the stopped driver, and the single rational reconstruction is progressive on the full path space.

  1. lemma OAI.SLEExactGauge.raw_rational_reconstruction_depends_on_past line 20
  2. theorem OAI.SLEExactGauge.exists_raw_progressive_radon_factor line 33