OAI/Analysis/CircleDomains/Transfer/PotentialPrescribedChartBound.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual barrier derivatives on almost every horizontal and vertical slice satisfy a common local bound by the physical density.

  1. theorem OAI.CircleDomainRigidity.potential_rectangle_derivative_bounds_with_constant line 21