OAI/Analysis/CircleDomains/Sobolev/PotentialLineDerivativeBound.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The actual path-bound potential has the expected derivative estimate on every physical chart line with finite density integral.

  1. theorem OAI.CircleDomainRigidity.potential_chart_lintegral_increment_bound line 18
  2. theorem OAI.CircleDomainRigidity.potential_chart_derivative_bound line 51