OAI/Analysis/CircleDomains/Sobolev/SmallSelectedBarrierEnergy.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Small selected-coordinate errors give a strict total source barrier bound, uniformly for any smooth barrier with the specified constants.

  1. theorem OAI.CircleDomainRigidity.CompactScalarModel.small_selected_barrier_energy line 15