OAI/Analysis/CircleDomains/Sobolev/ACLWeakDerivatives.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Integration by parts for the Borel representatives of ACL derivatives. This converts the actual slice derivative into a planar weak derivative.

  1. theorem OAI.CircleDomainRigidity.integral_mul_horizontal_deriv_eq_neg line 18
  2. theorem OAI.CircleDomainRigidity.integral_mul_vertical_deriv_eq_neg line 71