OAI/Analysis/CircleDomains/Sobolev/ScalarFlatteningWeak.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Distributional chain rule for the constructed flattening map. Smooth primitives converge with their bounded derivative multipliers, so the identity follows from the smooth chain rule.

  1. theorem OAI.CircleDomainRigidity.flattenValues_weak_partial line 14