FinitePatching.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Patching the finite family of filling disks

On pairwise disjoint open disks, replace the old coordinate by its smooth collar extension. Equality on full boundary neighborhoods gives smoothness across every boundary, and local equality preserves the rank-one wedge condition inside each filling disk.

def OAI.CircleDomainRigidity.FiniteTransfer.patchOpenRegions line 19
theorem OAI.CircleDomainRigidity.FiniteTransfer.patchOpenRegions_eq_of_mem line 24
theorem OAI.CircleDomainRigidity.FiniteTransfer.patchOpenRegions_eq_of_notMem line 35
theorem OAI.CircleDomainRigidity.FiniteTransfer.patchOpenRegions_eventuallyEq_inside line 40

theorem OAI.CircleDomainRigidity.FiniteTransfer.patchOpenRegions_eventuallyEq_outside line 50

Source documentation

Finiteness permits simultaneous agreement near a point lying outside all filling interiors, including a point on their boundaries.

theorem patchOpenRegions_eventuallyEq_outside
    {X Y I : Type*} [TopologicalSpace X] [Fintype I]
    (D : I → Set X) (g : I → X → Y) (f : X → Y)
    (hD : ∀ i, IsOpen (D i)) {x : X} (hx : ∀ i, x ∉ D i)
    (hagree : ∀ i, x ∈ frontier (D i) → g i =ᶠ[𝓝 x] f) :
    patchOpenRegions D g f =ᶠ[𝓝 x] f := by
…

Mentions: OAI.CircleDomainRigidity.FiniteTransfer.patchOpenRegions

theorem OAI.CircleDomainRigidity.FiniteTransfer.contDiffOn_patchOpenRegions line 72

Source documentation

Smoothness follows from smoothness of the old coordinate off the filling interiors and of each replacement inside its own disk.

theorem contDiffOn_patchOpenRegions
    {E I : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [Fintype I]
    (D : I → Set E) (g : I → E → ℝ) (f : E → ℝ)
    (hD : ∀ i, IsOpen (D i)) (hd : Pairwise (Disjoint on D))
    {U : Set E}
    (hf : ∀ x ∈ U, (∀ i, x ∉ D i) → ContDiffAt ℝ ∞ f x)
    (hg : ∀ i, ∀ x ∈ U ∩ D i, ContDiffAt ℝ ∞ (g i) x)
    (hagree : ∀ i, ∀ x ∈ U ∩ frontier (D i), g i =ᶠ[𝓝 x] f) :
    ContDiffOn ℝ ∞ (patchOpenRegions D g f) U := by
…

Mentions: OAI.CircleDomainRigidity.FiniteTransfer.patchOpenRegions

theorem OAI.CircleDomainRigidity.FiniteTransfer.patchOpenRegions_wedges_eq_zero_inside line 93

Source documentation

The patched family inherits each filling's pointwise zero wedges. The conclusion concerns actual derivatives of the patched functions.

theorem patchOpenRegions_wedges_eq_zero_inside
    {I L : Type*} (D : I → Set (ℝ × ℝ)) (g : I → L → (ℝ × ℝ) → ℝ)
    (f : L → (ℝ × ℝ) → ℝ) (hD : ∀ i, IsOpen (D i))
    (hd : Pairwise (Disjoint on D))
    (hzero : ∀ i j k, j ≠ k → ∀ x ∈ D i,
      planarWedge (planarGradient (g i j) x) (planarGradient (g i k) x) = 0)
    {i : I} {x : ℝ × ℝ} (hx : x ∈ D i) (j k : L) (hjk : j ≠ k) :
    planarWedge
      (planarGradient (patchOpenRegions D (fun i => g i j) (f j)) x)
      (planarGradient (patchOpenRegions D (fun i => g i k) (f k)) x) = 0 := by
…

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