OAI/Analysis/LipschitzHilbert/Estimates/VariationMeanOscillation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The local BMO step for variation: short-scale L1 control and long-scale oscillation control imply mean oscillation of the full variation.

  1. theorem OAI.LipschitzHilbert.variation_short_long_mean_oscillation line 14