OAI/Analysis/CircleDomains/Modulus/SquareQuarterOscillation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Pointwise control by the mean oscillations on quarter-scale squares. The geometric decay is matched to square-integrable energy.

  1. lemma OAI.CircleDomainRigidity.squareAverage_quartering line 12
  2. lemma OAI.CircleDomainRigidity.square_point_average_bound_quarters line 27