OAI/Analysis/CircleDomains/Sobolev/PartitionLiftApproximation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Actual smooth approximants of the local real branches, preserving interval bounds and prescribed weighted L2 derivative errors.

  1. theorem OAI.CircleDomainRigidity.exists_partition_lift_approximants line 16
  2. theorem OAI.CircleDomainRigidity.exists_partition_lift_approximants_with_accuracy line 66