OAI/Analysis/CircleDomains/Topology/BoundaryPairNeighborhood.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Open exclusion neighborhoods use the actual fixed-source boundary functional. Its continuity is proved from the disk-distance estimate; no stability or exclusion assertion is assumed.

  1. abbrev OAI.CircleDomainRigidity.BoundaryPairData line 18
  2. def OAI.CircleDomainRigidity.boundaryPairFunctional line 20
  3. def OAI.CircleDomainRigidity.boundaryCurveTrace line 23
  4. theorem OAI.CircleDomainRigidity.boundaryPairFunctional_trace line 26
  5. theorem OAI.CircleDomainRigidity.boundaryPairFunctional_lipschitz line 36
  6. theorem OAI.CircleDomainRigidity.continuous_boundaryPairFunctional line 62
  7. def OAI.CircleDomainRigidity.boundaryExclusionSet line 67

    Source documentation

    This is the open set excluded by a single retained period coordinate.

    def boundaryExclusionSet (v : ℝ → ℝ) (budget : ℝ) : Set BoundaryPairData :=
…

    Mentions: OAI.CircleDomainRigidity.BoundaryPairData

  8. theorem OAI.CircleDomainRigidity.isOpen_boundaryExclusionSet line 70
  9. theorem OAI.CircleDomainRigidity.boundaryExclusionSet_excludes_stokes_limit line 75