OAI/Probability/SLE/Mass/MassKernelUniqueness.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Equal terminal remainder kernels yield a martingale difference; continuity and increasing integrable masses then imply uniqueness.

  1. lemma OAI.SLEExactGauge.mass_difference_martingale_of_terminal_mean line 17
  2. theorem OAI.SLEExactGauge.increasing_mass_unique_of_terminal_mean line 32