RankOneFilling.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Rank-one smooth filling of a collar

If at most one coordinate varies on a collar, extend that coordinate by a smooth cutoff and all the others constantly. Every pairwise wedge of the resulting coordinate gradients vanishes throughout the filling.

def OAI.CircleDomainRigidity.FiniteTransfer.planarGradient line 21
theorem OAI.CircleDomainRigidity.FiniteTransfer.planarGradient_const line 24

theorem OAI.CircleDomainRigidity.FiniteTransfer.exists_rank_one_collar_extension line 30

Source documentation

The scalar collar extension gives a simultaneous smooth extension with zero pairwise wedges when only one boundary coordinate is active.

theorem exists_rank_one_collar_extension {ι : Type*} (k : ι)
    {U A : Set (ℝ × ℝ)} (hU : IsOpen U) (hA : IsClosed A) (hAU : A ⊆ U)
    (f : ι → (ℝ × ℝ) → ℝ) (c : ι → ℝ)
    (hfk : ContDiffOn ℝ ∞ (f k) U)
    (hinactive : ∀ i, i ≠ k → EqOn (f i) (fun _ => c i) U) :
    ∃ F : ι → (ℝ × ℝ) → ℝ,
      (∀ i, ContDiff ℝ ∞ (F i)) ∧
      (∀ᶠ x in 𝓝ˢ A, ∀ i, F i x = f i x) ∧
      (∀ i x, x ∉ U → F i x = c i) ∧
      (∀ i j, i ≠ j → ∀ x, planarWedge (planarGradient (F i) x)
        (planarGradient (F j) x) = 0) := by
…

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