OAI/Probability/SLE/Loewner/RawTerminalExhaustion.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

A measurable terminal certificate for the raw finite-time mass. Together with monotonicity it yields terminal domination and local exhaustion at all real times, not just integer times.

  1. lemma OAI.SLEExactGauge.ennreal_antitone_tendsto_zero_of_nat line 20
  2. def OAI.SLEExactGauge.RawTerminalGood line 29
  3. theorem OAI.SLEExactGauge.measurableSet_rawTerminalGood line 34
  4. theorem OAI.SLEExactGauge.RawTerminalGood.domination_exhaustion line 57
  5. theorem OAI.SLEExactGauge.rawTerminalGood_of_exhaustion line 89
  6. theorem OAI.SLEExactGauge.Multipoint.CanonicalMass.raw_terminal_good_set line 112