OAI/Analysis/CircleDomains/Topology/CirclePatching.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Patching circle coordinates across filling disks

Real collar extensions project to genuine circle maps. Equality of the projections on full boundary neighborhoods suffices for smooth patching; global real branches on the retained region are unnecessary.

  1. theorem OAI.CircleDomainRigidity.FiniteTransfer.smoothCircleOn_patchOpenRegions line 21
  2. theorem OAI.CircleDomainRigidity.FiniteTransfer.circleGradient_patchOpenRegions_inside line 44
  3. theorem OAI.CircleDomainRigidity.FiniteTransfer.circleGradient_patchOpenRegions_outside line 59
  4. theorem OAI.CircleDomainRigidity.FiniteTransfer.circle_patch_wedges_eq_zero_inside line 72

    Source documentation

    Rank-one real extensions retain their zero-wedge property after projection and patching into the original circle coordinates.

    theorem circle_patch_wedges_eq_zero_inside
    {I L : Type*} (D : I → Set (ℝ × ℝ)) (hD : ∀ i, IsOpen (D i))
    (hdisj : Pairwise (Disjoint on D))
    (f : L → (ℝ × ℝ) → UnitAddCircle) (g : I → L → (ℝ × ℝ) → ℝ)
    (hg : ∀ i l, ContDiff ℝ ∞ (g i l))
    (hzero : ∀ i l m, l ≠ m → ∀ x ∈ D i,
      planarWedge (planarGradient (g i l) x) (planarGradient (g i m) x) = 0)
    {i : I} {x : ℝ × ℝ} (hx : x ∈ D i) (l m : L) (hlm : l ≠ m) :
    planarWedge
      (circleGradient (patchOpenRegions D (fun i x => (g i l x : UnitAddCircle)) (f l)) x)
      (circleGradient (patchOpenRegions D (fun i x => (g i m x : UnitAddCircle)) (f m)) x) = 0 := by
…

    Mentions: OAI.CircleDomainRigidity.FiniteTransfer.planarWedge, OAI.CircleDomainRigidity.FiniteTransfer.planarGradient, OAI.CircleDomainRigidity.FiniteTransfer.circleGradient, OAI.CircleDomainRigidity.FiniteTransfer.patchOpenRegions