OAI/Analysis/CircleDomains/Modulus/AverageOscillation.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Elementary mean-oscillation bounds used for Sobolev square averages.

  1. lemma OAI.CircleDomainRigidity.average_mono_real line 11
  2. lemma OAI.CircleDomainRigidity.abs_average_le_average_abs line 17
  3. lemma OAI.CircleDomainRigidity.abs_sub_average_le_average_abs_sub line 22
  4. lemma OAI.CircleDomainRigidity.abs_sub_average_le_of_ae line 32