OAI/Analysis/CircleDomains/Sobolev/PositivePartitionSmoothing.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Positive smoothing on an open plane domain with a prescribed sum of local gradient errors. All approximants and partition weights are constructed.

  1. theorem OAI.CircleDomainRigidity.exists_positive_partition_smoothing line 15