OAI/Analysis/CircleDomains/Topology/CompactScalarContinuation.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Scalar tests vanishing near the source end at infinity continue with compact planar support. Their global planar Sobolev witness has the actual weak fields, which vanish off the limiting domain.

  1. theorem OAI.CircleDomainRigidity.RetainedRealCircleModel.continuedScalar_on_end line 21
  2. theorem OAI.CircleDomainRigidity.RetainedRealCircleModel.continuedScalar_zero_near_infty line 29
  3. theorem OAI.CircleDomainRigidity.RetainedRealCircleModel.continuedScalar_hasCompactSupport line 42
  4. def OAI.CircleDomainRigidity.RetainedRealCircleModel.ScalarWeakLimit.continuedScalar_witness line 52