OAI/Analysis/CircleDomains/Sobolev/LineLIntegralDerivativeBound.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The path inequality is naturally extended-valued. On each finite slice it bounds the ordinary derivative by the real density.

  1. theorem OAI.CircleDomainRigidity.ae_abs_deriv_le_of_lintegral_bound line 14