OAI/Analysis/CircleDomains/Sobolev/SphereScalarLineSmooth.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Smoothness on the domain of the actual finite chart and of a compact smooth scalar pulled back along either source axis.

  1. theorem OAI.CircleDomainRigidity.MatchedConformalEnds.finite_part_contDiffOn line 18
  2. theorem OAI.CircleDomainRigidity.MatchedConformalEnds.sphere_scalar_line_contDiffOn line 26