OAI/Analysis/CircleDomains/Sobolev/PartitionApproximation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Select one positive local smoothing on each compact partition core, with prescribed weighted derivative error in both coordinate directions.

  1. theorem OAI.CircleDomainRigidity.exists_partition_smooth_approximants line 16