OAI/Analysis/CircleDomains/Probability/LocalHorizontalNullPair.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The horizontal trace-pair lemma is local in the Sobolev coordinate. A compact plateau reduces it to the global trace-pair statement.

  1. theorem OAI.CircleDomainRigidity.local_sobolev_horizontal_pair_null_image line 13