OAI/Probability/SLE/Mass/TerminalMassTestLimit.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Local exhaustion implies convergence of every compact continuous test. This provides the terminal value of the fixed raw driver functional.

  1. lemma OAI.SLEExactGauge.compact_test_norm_le_mass line 16
  2. theorem OAI.SLEExactGauge.terminal_mass_test_tendsto line 29