OAI/Analysis/CircleDomains/Sobolev/CompactIntegralComparison.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A finite measurable slice density is controlled almost everywhere when all of its compact-set integrals are controlled.

  1. theorem OAI.CircleDomainRigidity.ae_le_of_compact_setLIntegral_le line 16