OAI/Analysis/LipschitzHilbert/Estimates/MeanOscillation.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Local mean oscillation estimates used before John--Nirenberg. The short part is controlled in mean and the long part by its oscillation. All constants are independent of the dimension of the range.

  1. def OAI.LipschitzHilbert.integralAverage line 18
  2. theorem OAI.LipschitzHilbert.norm_average_sub_le line 21
  3. theorem OAI.LipschitzHilbert.integral_oscillation_le_twice line 31
  4. theorem OAI.LipschitzHilbert.integralAverage_add line 53
  5. theorem OAI.LipschitzHilbert.short_long_mean_oscillation line 58