OAI/Analysis/CircleDomains/Modulus/RectangleMeanOscillation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The L1 rectangular Poincare estimate, in normalized-average form.

  1. lemma OAI.CircleDomainRigidity.rectangle_mean_oscillation line 12