OAI/Analysis/CircleDomains/Sobolev/SquarePoincareEnergy.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A square's mean oscillation squared is bounded by its actual local Sobolev energy. The radius cancels against the square's area.

  1. lemma OAI.CircleDomainRigidity.local_partial_coordinate_memLp line 13
  2. lemma OAI.CircleDomainRigidity.locally_sobolev_square_oscillation_sq line 26