OAI/Probability/SLE/Geometry/CanonicalRawMean.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The fixed raw terminal functional has the exact Green mean under the driver law. Strong Markov then allows arbitrary stopped-past spatial weights in the fresh terminal mass.

  1. theorem OAI.SLEExactGauge.Multipoint.CanonicalMass.raw_terminal_mean line 19
  2. theorem OAI.SLEExactGauge.Multipoint.CanonicalMass.restarted_raw_terminal_mean line 37
  3. theorem OAI.SLEExactGauge.Multipoint.CanonicalMass.fresh_terminal_random_test line 65