OAI/Analysis/CircleDomains/Rigidity/SmoothMatchedScalar.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A compact smooth target scalar supplies all analytic hypotheses of the actual matched mask. In particular its source differential is L².

  1. theorem OAI.CircleDomainRigidity.smooth_compact_sphere_scalar line 18
  2. theorem OAI.CircleDomainRigidity.MatchedConformalEnds.smooth_selected_scalar_finite_energy line 42