OAI/Analysis/LipschitzHilbert/Fourier/VariationLineBMO.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Applying the interval John--Nirenberg theorem to a finite packet variation, using the actual short/long decomposition on each cell.

  1. theorem OAI.LipschitzHilbert.FiniteLineGrid.continuous_integrable_cell line 17
  2. theorem OAI.LipschitzHilbert.FiniteLineGrid.variation_full_mean_oscillation line 22
  3. theorem OAI.LipschitzHilbert.FiniteLineGrid.variation_centered_line_moment line 55