OAI/Analysis/LipschitzHilbert/Estimates/ContinuousBMOTail.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

John--Nirenberg's geometric distribution bound for a continuous function on an actual finite interval. The proof passes the uniform finite grid estimate to the function, using pointwise convergence of cell means.

  1. def OAI.LipschitzHilbert.FiniteLineGrid.HasFullMeanOscillationBound line 18
  2. theorem OAI.LipschitzHilbert.FiniteLineGrid.continuous_mean_oscillation_tail line 22