ComplexWeakDirectionalTransport.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Transport a complex distributional directional derivative to each real component of the physical weak gradient. Only smooth compact tests and local integrability enter this bridge.

lemma OAI.CircleDomainRigidity.weakPartial_of_complex_directional_identity line 14