OAI/Probability/SLE/Stochastic/BrownianOptionalInequality.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A one-sided optional-stopping estimate for the discounted multipoint product, obtained from the centered grid identity and the sign of the drift.

  1. lemma OAI.SLEExactGauge.bounded_cumulative_at_grid_le line 14
  2. theorem OAI.SLEExactGauge.brownian_time_field_optional_le line 42