OAI/Analysis/LipschitzHilbert/Trees/LineGridConditionalBMO.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The concrete cellwise mean-oscillation bound implies the conditional oscillation hypothesis used by the finite martingale stopping argument.

  1. theorem OAI.LipschitzHilbert.FiniteLineGrid.integrated_oscillation_le line 15
  2. theorem OAI.LipschitzHilbert.FiniteLineGrid.terminal_mean_oscillation line 44