OAI/Analysis/CircleDomains/Sobolev/LineLIntegralAbsoluteContinuity.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The line-integral criterion in extended nonnegative form. It applies directly to the measurable path densities used by the barrier.

  1. theorem OAI.CircleDomainRigidity.absolutelyContinuousOnInterval_of_lintegral_bound line 17