OAI/Analysis/CircleDomains/Sobolev/WeightedSmoothContours.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Smooth obstacle-isolating contours whose actual Hausdorff arclength integral against the prescribed density is finite.

  1. theorem OAI.CircleDomainRigidity.exists_weighted_regular_isolating_obstacle line 16
  2. theorem OAI.CircleDomainRigidity.exists_finite_weighted_contours_isolating_obstacle line 57