CollarExtension.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Smooth extension of the active filling coordinate

A real branch smooth on a collar can be retained on a smaller closed collar and extended to be constant away from it. In a filling disk all other branches are constant, so this is the only extension needed there.

theorem OAI.CircleDomainRigidity.FiniteTransfer.contDiff_collar_cutoff line 23

Source documentation

Multiplication by a smooth cutoff which vanishes near the complement of U makes a branch smooth globally. No regularity of the branch is required outside its original open domain.

theorem contDiff_collar_cutoff {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    {U : Set E} {f χ : E → ℝ} {n : ℕ∞} (hU : IsOpen U)
    (hf : ContDiffOn ℝ n f U) (hχ : ContDiff ℝ n χ)
    (hzero : ∀ᶠ x in 𝓝ˢ Uᶜ, χ x = 0) (c : ℝ) :
    ContDiff ℝ n (fun x => c + χ x * (f x - c)) := by
…

theorem OAI.CircleDomainRigidity.FiniteTransfer.exists_smooth_collar_extension line 40

Source documentation

Retain an arbitrary smooth real branch near a closed collar inside its domain, and make it constant off that domain.

theorem exists_smooth_collar_extension {E : Type*} [NormedAddCommGroup E]
    [NormedSpace ℝ E] [FiniteDimensional ℝ E]
    {U A : Set E} (hU : IsOpen U) (hA : IsClosed A) (hAU : A ⊆ U)
    {f : E → ℝ} (hf : ContDiffOn ℝ ∞ f U) (c : ℝ) :
    ∃ F : E → ℝ, ContDiff ℝ ∞ F ∧ F =ᶠ[𝓝ˢ A] f ∧ ∀ x ∉ U, F x = c := by
…