OAI/Analysis/CircleDomains/Selection/LocalizedPhysicalPlateaus.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Exact plateaus and bands with both global and localized gradient estimates.

  1. theorem OAI.CircleDomainRigidity.potential_physical_smoothing_with_localized_plateaus line 20