OAI/Analysis/LipschitzHilbert/Estimates/MartingaleGoodLambda.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A first-crossing contraction for a finite martingale with bounded conditional mean oscillation. This is the finite stopping step in the John--Nirenberg proof; no exponential-tail theorem is assumed.

  1. def OAI.LipschitzHilbert.TerminalMeanOscillationBound line 20
  2. theorem OAI.LipschitzHilbert.martingale_goodLambda line 25