OAI/Analysis/CircleDomains/Sobolev/IntegralLineAbsoluteContinuity.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A linewise integral bound yields actual absolute continuity, without first choosing a measurable representative for the bounded potential.

  1. theorem OAI.CircleDomainRigidity.absolutelyContinuousOnInterval_of_dist_le line 15
  2. theorem OAI.CircleDomainRigidity.absolutelyContinuousOnInterval_of_integral_bound line 27