OAI/Analysis/CircleDomains/Sobolev/LocalizedPotentialSmoothing.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Positive smoothing with a localized energy estimate, retaining the global finite-energy assertion.

  1. theorem OAI.CircleDomainRigidity.potential_positive_partition_smoothing_with_local_energy line 17