OAI/Analysis/CircleDomains/Sobolev/SupportedMetric.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Metric changes with compact support

The original core may be unbounded in a planar chart, as happens when the retained spherical core contains infinity. Only its intersection with a compact neighborhood of the completed piece is needed for the interpolation. A second cutoff keeps the metric unchanged at infinity.

  1. theorem OAI.CircleDomainRigidity.FiniteTransfer.blendMetric_identity line 21
  2. theorem OAI.CircleDomainRigidity.FiniteTransfer.exists_supported_metric_for_local_coordinates line 25