OAI/Analysis/CircleDomains/Sobolev/CoordinateSquares.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Coordinate squares, their exact areas, and the actual Sobolev Poincare estimate.

  1. def OAI.CircleDomainRigidity.coordinateSquare line 11
  2. lemma OAI.CircleDomainRigidity.coordinateSquare_eq_rectangle line 13
  3. lemma OAI.CircleDomainRigidity.coordinateSquare_compact line 18
  4. lemma OAI.CircleDomainRigidity.coordinateSquare_real_volume line 21
  5. lemma OAI.CircleDomainRigidity.coordinateSquare_volume_ne_zero line 30
  6. lemma OAI.CircleDomainRigidity.locally_sobolev_square_poincare line 37