OAI/Analysis/CircleDomains/Probability/HorizontalNullPair.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The companion trace pair with the ordinary horizontal coordinate. The same proved level argument applies to the constant rotated homeomorphism.

  1. def OAI.CircleDomainRigidity.horizontalLinear line 12
  2. theorem OAI.CircleDomainRigidity.horizontalLinear_apply line 15
  3. def OAI.CircleDomainRigidity.horizontalGradient line 17
  4. theorem OAI.CircleDomainRigidity.horizontal_weak_gradient line 20
  5. theorem OAI.CircleDomainRigidity.horizontal_gradient_memLp line 29
  6. theorem OAI.CircleDomainRigidity.horizontal_as_height line 37
  7. theorem OAI.CircleDomainRigidity.sobolev_horizontal_pair_null_image line 46