contDiffBump — Mathlib

English

Let E and X be normed spaces with a continuous-diff bump structure on E. Suppose c: X → E, f: ∀x, ContDiffBump(c(x)), s ⊆ X, x ∈ s, and n ∈ ℕ∞. If c is Cn on s, the rIn and rOut radii associated to f(x) are Cn in s via rIn and rOut, and g: X → E is Cn on s, then the map x ↦ f(x)(g(x)) is Cn on s (i.e. ContDiffWithinAt ℝ n of order n for all x in s).

Русский

Пусть E, X – нормированные группы, имеется выпукло-аналоговая функция (бамп) на E, пусть c: X → E, f: ∀x, ContDiffBump (c(x)), s ⊆ X, x ∈ s и n ∈ ℕ∞. Если c непрерывно-дифференцируема порядка n на s, соответствующие радиусы rIn, rOut функции f(x) также зависят гладко по x на s, и g: X → E непрерывно дифференцируема порядка n на s, то отображение x ↦ f(x)(g(x)) образует функцию, гладкую до порядка n на s (ContDiffWithinAt ℝ n).

LaTeX

$$$\\forall E X \\,[\\text{NormedAddCommGroup } E]\\, [\\text{NormedSpace } \\mathbb{R}E]\\, [\\text{NormedAddCommGroup } X]\\, [\\text{NormedSpace } \\mathbb{R}X] \\, [\\HasContDiffBump E]\\, {c:X\\to E}\\, {f: \\forall x, ContDiffBump (c x)}{s:\\ Set X}{x:X}\\, {n: \\mathbb{N}_{\\infty}} \\,\nrightarrow\ \ ContDiffWithinAt\\,\\mathbb{R}\\, n\\, c\\, s\\, x \\,\\to\\n\\rightarrow\ ContDiffWithinAt\\,\\mathbb{R}\\, n\\, (fun x => (f x).rIn)\\, s\\, x \\,\\to\\n\\rightarrow\ ContDiffWithinAt\\,\\mathbb{R}\\, n\\, (fun x => (f x).rOut)\\, s\\, x \\,\\to\\n\\rightarrow\ ContDiffWithinAt\\,\\mathbb{R}\\, n\\, g\\, s\\, x \\,\\to\\n\\rightarrow\ ContDiffWithinAt\\,\\mathbb{R}\\, n\\, (fun x => (f x) (g x))\\, s\\, x$$$

Lean4

/-- `ContDiffBump` is `𝒞ⁿ` in all its arguments. -/
protected theorem _root_.ContDiffWithinAt.contDiffBump {c g : X → E} {s : Set X} {f : ∀ x, ContDiffBump (c x)} {x : X}
    (hc : ContDiffWithinAt ℝ n c s x) (hr : ContDiffWithinAt ℝ n (fun x => (f x).rIn) s x)
    (hR : ContDiffWithinAt ℝ n (fun x => (f x).rOut) s x) (hg : ContDiffWithinAt ℝ n g s x) :
    ContDiffWithinAt ℝ n (fun x => f x (g x)) s x :=
  by
  change
    ContDiffWithinAt ℝ n
      (uncurry (someContDiffBumpBase E).toFun ∘ fun x : X => ((f x).rOut / (f x).rIn, (f x).rIn⁻¹ • (g x - c x))) s x
  refine (((someContDiffBumpBase E).smooth.contDiffAt ?_).of_le (mod_cast le_top)).comp_contDiffWithinAt x ?_
  · exact prod_mem_nhds (Ioi_mem_nhds (f x).one_lt_rOut_div_rIn) univ_mem
  · exact (hR.div hr (f x).rIn_pos.ne').prodMk ((hr.inv (f x).rIn_pos.ne').smul (hg.sub hc))

Похожие утверждения