OAI/Analysis/CircleDomains/Topology/CompactPairChainRule.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The joint smooth chain rule for the actual continuous compact source coordinates. Positive mollification converges pointwise and in gradient L2, so the two coefficient products pass to the weak derivative.

  1. theorem OAI.CircleDomainRigidity.compact_pair_weak_chain line 15