OAI/Analysis/CircleDomains/Sobolev/ModelSmoothBarrier.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A smooth compact target barrier has its actual smooth source Sobolev witness and no greater Dirichlet energy, by conformal transport.

  1. theorem OAI.CircleDomainRigidity.CompactScalarModel.smooth_barrier_pullback line 18