OAI/Analysis/CircleDomains/Sobolev/RationalLineDerivative.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The same rational interval estimates control the almost-everywhere ordinary derivative by the actual measurable line density.

  1. theorem OAI.CircleDomainRigidity.locally_ae_abs_deriv_le_of_rational_bounds line 14