OAI/Analysis/CircleDomains/Sobolev/BoundedLocalBranches.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Local bounded lifts can be used in the compact-band construction by setting them to zero outside their patch. Their bands, local continuity, and physical derivatives within the open patch are unchanged.

  1. def OAI.CircleDomainRigidity.localBranchRepresentative line 17
  2. theorem OAI.CircleDomainRigidity.localBranchRepresentative_bound line 19
  3. theorem OAI.CircleDomainRigidity.localBranchRepresentative_eventuallyEq line 28
  4. theorem OAI.CircleDomainRigidity.localBranchRepresentative_circle_band line 35
  5. theorem OAI.CircleDomainRigidity.localBranchRepresentative_continuousOn line 48
  6. theorem OAI.CircleDomainRigidity.localBranchRepresentative_contDiffOn line 55