OAI/Analysis/CircleDomains/Rigidity/IntervalTraceExtension.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Endpoint traces from finite variation on an open interval

A differentiable function on an open bounded interval whose derivative is integrable has an absolutely continuous extension to the closed interval. This supplies the endpoint traces at the round holes in the parallel-line argument, without assuming boundary continuity.

  1. theorem OAI.CircleDomainRigidity.exists_absolutelyContinuous_extension_of_integrable_derivative line 19
  2. theorem OAI.CircleDomainRigidity.exists_absolutelyContinuous_extension_of_memLp_derivative line 62