OAI/Analysis/CircleDomains/Sobolev/SquareOscillationLipschitz.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform square mean-oscillation bounds give a quantitative Lipschitz restriction.

  1. lemma OAI.CircleDomainRigidity.square_oscillation_lipschitzOn line 11
  2. lemma OAI.CircleDomainRigidity.locally_sobolev_lipschitzOn_of_square_averages line 48