Mathlib.Analysis.Calculus.ContDiff.Operations

hasFTaylorSeriesUpToOn_pi theorem

 {n : WithTop ℕ∞} :
  HasFTaylorSeriesUpToOn n (fun x i => φ i x) (fun x m => ContinuousMultilinearMap.pi fun i => p' i x m) s ↔
    ∀ i, HasFTaylorSeriesUpToOn n (φ i) (p' i) s

Full source

theorem hasFTaylorSeriesUpToOn_pi {n : WithTop ℕ∞} :
    HasFTaylorSeriesUpToOnHasFTaylorSeriesUpToOn n (fun x i => φ i x)
        (fun x m => ContinuousMultilinearMap.pi fun i => p' i x m) s ↔
      ∀ i, HasFTaylorSeriesUpToOn n (φ i) (p' i) s := by
  set pr := @ContinuousLinearMap.proj 𝕜 _ ι F' _ _ _
  set L : ∀ m : ℕ, (∀ i, E[×m]→L[𝕜] F' i) ≃ₗᵢ[𝕜] E[×m]→L[𝕜] ∀ i, F' i := fun m =>
    ContinuousMultilinearMap.piₗᵢ _ _
  refine ⟨fun h i => ?_, fun h => ⟨fun x hx => ?_, ?_, ?_⟩⟩
  · exact h.continuousLinearMap_comp (pr i)
  · ext1 i
    exact (h i).zero_eq x hx
  · intro m hm x hx
    exact (L m).hasFDerivAt.comp_hasFDerivWithinAt x <|
      hasFDerivWithinAt_pi.2 fun i => (h i).fderivWithin m hm x hx
  · intro m hm
    exact (L m).continuous.comp_continuousOn <| continuousOn_pi.2 fun i => (h i).cont m hm

Product of functions has Taylor series if and only if each component does

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $E$ a normed space over $\mathbb{K}$, and $F' = \prod_{i \in \iota} F'_i$ a finite product of normed spaces over $\mathbb{K}$. For each $i \in \iota$, let $\varphi_i : E \to F'_i$ be a function with a formal Taylor series $p'_i$ up to order $n$ on a subset $s \subseteq E$. Then the product function $\Phi(x) = (\varphi_i(x))_{i \in \iota}$ has a formal Taylor series up to order $n$ on $s$ (given by the product of the $p'_i$) if and only if each $\varphi_i$ has a formal Taylor series up to order $n$ on $s$.

hasFTaylorSeriesUpToOn_pi' theorem

 {n : WithTop ℕ∞} :
  HasFTaylorSeriesUpToOn n Φ P' s ↔
    ∀ i,
      HasFTaylorSeriesUpToOn n (fun x => Φ x i)
        (fun x m => (@ContinuousLinearMap.proj 𝕜 _ ι F' _ _ _ i).compContinuousMultilinearMap (P' x m)) s

Full source

@[simp]
theorem hasFTaylorSeriesUpToOn_pi' {n : WithTop ℕ∞} :
    HasFTaylorSeriesUpToOnHasFTaylorSeriesUpToOn n Φ P' s ↔
      ∀ i, HasFTaylorSeriesUpToOn n (fun x => Φ x i)
        (fun x m => (@ContinuousLinearMap.proj 𝕜 _ ι F' _ _ _ i).compContinuousMultilinearMap
          (P' x m)) s := by
  convert hasFTaylorSeriesUpToOn_pi (𝕜 := 𝕜) (φ := fun i x ↦ Φ x i); ext; rfl

Componentwise Characterization of Taylor Series for Product-Valued Functions

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $E$ a normed space over $\mathbb{K}$, and $F' = \prod_{i \in \iota} F'_i$ a finite product of normed spaces over $\mathbb{K}$. Given a function $\Phi : E \to F'$ and a family of formal Taylor series $P'$ for $\Phi$ up to order $n$ on a subset $s \subseteq E$, the following are equivalent: 1. $\Phi$ has a formal Taylor series up to order $n$ on $s$ given by $P'$. 2. For each $i \in \iota$, the component function $x \mapsto \Phi(x)_i$ has a formal Taylor series up to order $n$ on $s$, obtained by composing $P'$ with the $i$-th projection map from $F'$ to $F'_i$.

contDiffWithinAt_pi theorem

: ContDiffWithinAt 𝕜 n Φ s x ↔ ∀ i, ContDiffWithinAt 𝕜 n (fun x => Φ x i) s x

Full source

theorem contDiffWithinAt_pi :
    ContDiffWithinAtContDiffWithinAt 𝕜 n Φ s x ↔ ∀ i, ContDiffWithinAt 𝕜 n (fun x => Φ x i) s x := by
  set pr := @ContinuousLinearMap.proj 𝕜 _ ι F' _ _ _
  refine ⟨fun h i => h.continuousLinearMap_comp (pr i), fun h ↦ ?_⟩
  match n with
  | ω =>
    choose u hux p hp h'p using h
    refine ⟨⋂ i, u i, Filter.iInter_mem.2 hux, _,
      hasFTaylorSeriesUpToOn_pi.2 fun i => (hp i).mono <| iInter_subset _ _, fun m ↦ ?_⟩
    set L : (∀ i, E[×m]→L[𝕜] F' i) ≃ₗᵢ[𝕜] E[×m]→L[𝕜] ∀ i, F' i :=
      ContinuousMultilinearMap.piₗᵢ _ _
    change AnalyticOn 𝕜 (fun x ↦ L (fun i ↦ p i x m)) (⋂ i, u i)
    apply (L.analyticOnNhd univ).comp_analyticOn ?_ (mapsTo_univ _ _)
    exact AnalyticOn.pi (fun i ↦ (h'p i m).mono (iInter_subset _ _))
  | (n : ℕ∞) =>
    intro m hm
    choose u hux p hp using fun i => h i m hm
    exact ⟨⋂ i, u i, Filter.iInter_mem.2 hux, _,
      hasFTaylorSeriesUpToOn_pi.2 fun i => (hp i).mono <| iInter_subset _ _⟩

Componentwise $C^n$ Differentiability of Product-Valued Functions on a Set at a Point

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $E$ a normed space over $\mathbb{K}$, and $F = \prod_{i \in \iota} F_i$ a finite product of normed spaces over $\mathbb{K}$. For a function $\Phi : E \to F$ and a point $x \in E$, the following are equivalent: 1. $\Phi$ is $C^n$ within a set $s \subseteq E$ at $x$. 2. For each $i \in \iota$, the component function $x \mapsto \Phi(x)_i$ is $C^n$ within $s$ at $x$. Here, $C^n$ denotes $n$-times continuous differentiability (or analyticity when $n = \omega$).

contDiffOn_pi theorem

: ContDiffOn 𝕜 n Φ s ↔ ∀ i, ContDiffOn 𝕜 n (fun x => Φ x i) s

Full source

theorem contDiffOn_pi : ContDiffOnContDiffOn 𝕜 n Φ s ↔ ∀ i, ContDiffOn 𝕜 n (fun x => Φ x i) s :=
  ⟨fun h _ x hx => contDiffWithinAt_pi.1 (h x hx) _, fun h x hx =>
    contDiffWithinAt_pi.2 fun i => h i x hx⟩

Componentwise $C^n$ Differentiability of Product-Valued Functions on a Set

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $E$ a normed space over $\mathbb{K}$, and $F = \prod_{i \in \iota} F_i$ a finite product of normed spaces over $\mathbb{K}$. For a function $\Phi : E \to F$ and a subset $s \subseteq E$, the following are equivalent: 1. $\Phi$ is $C^n$ on $s$. 2. For each $i \in \iota$, the component function $x \mapsto \Phi(x)_i$ is $C^n$ on $s$. Here, $C^n$ denotes $n$-times continuous differentiability (or analyticity when $n = \omega$).

contDiffAt_pi theorem

: ContDiffAt 𝕜 n Φ x ↔ ∀ i, ContDiffAt 𝕜 n (fun x => Φ x i) x

Full source

theorem contDiffAt_pi : ContDiffAtContDiffAt 𝕜 n Φ x ↔ ∀ i, ContDiffAt 𝕜 n (fun x => Φ x i) x :=
  contDiffWithinAt_pi

Componentwise $C^n$ Differentiability of Product-Valued Functions at a Point

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $E$ a normed space over $\mathbb{K}$, and $F = \prod_{i \in \iota} F_i$ a finite product of normed spaces over $\mathbb{K}$. For a function $\Phi : E \to F$ and a point $x \in E$, the following are equivalent: 1. $\Phi$ is $C^n$ at $x$. 2. For each $i \in \iota$, the component function $x \mapsto \Phi(x)_i$ is $C^n$ at $x$. Here, $C^n$ denotes $n$-times continuous differentiability (or analyticity when $n = \omega$).

contDiff_pi theorem

: ContDiff 𝕜 n Φ ↔ ∀ i, ContDiff 𝕜 n fun x => Φ x i

Full source

theorem contDiff_pi : ContDiffContDiff 𝕜 n Φ ↔ ∀ i, ContDiff 𝕜 n fun x => Φ x i := by
  simp only [← contDiffOn_univ, contDiffOn_pi]

$C^n$-differentiability of product-space-valued functions via componentwise differentiability

Informal description

A function $\Phi : E \to \prod_{i} F'_i$ between normed spaces is $C^n$-differentiable if and only if for every index $i$, the component function $x \mapsto \Phi(x)_i$ is $C^n$-differentiable.

contDiff_update theorem

[DecidableEq ι] (k : WithTop ℕ∞) (x : ∀ i, F' i) (i : ι) : ContDiff 𝕜 k (update x i)

Full source

theorem contDiff_update [DecidableEq ι] (k : WithTop ℕ∞) (x : ∀ i, F' i) (i : ι) :
    ContDiff 𝕜 k (update x i) := by
  rw [contDiff_pi]
  intro j
  dsimp [Function.update]
  split_ifs with h
  · subst h
    exact contDiff_id
  · exact contDiff_const

$C^k$-differentiability of function updates in product spaces

Informal description

Let $\iota$ be a finite index type with decidable equality, and let $F'$ be a family of normed spaces over a nontrivially normed field $\mathbb{K}$. For any extended natural number $k \in \mathbb{N}_\infty$, any element $x \in \prod_{i \in \iota} F'_i$, and any index $i \in \iota$, the function update operation $\text{update } x \, i : F'_i \to \prod_{i \in \iota} F'_i$ is $C^k$-differentiable. Here, $\text{update } x \, i$ denotes the function that maps a value $v \in F'_i$ to the element of $\prod_{i \in \iota} F'_i$ which equals $x$ everywhere except at index $i$, where it takes the value $v$.

contDiff_single theorem

[DecidableEq ι] (k : WithTop ℕ∞) (i : ι) : ContDiff 𝕜 k (Pi.single i : F' i → ∀ i, F' i)

Full source

theorem contDiff_single [DecidableEq ι] (k : WithTop ℕ∞) (i : ι) :
    ContDiff 𝕜 k (Pi.single i : F' i → ∀ i, F' i) :=
  contDiff_update k 0 i

$C^k$-Differentiability of Single-Element Injection in Product Spaces

Informal description

Let $\iota$ be a finite index type with decidable equality, and let $F'$ be a family of normed spaces over a nontrivially normed field $\mathbb{K}$. For any extended natural number $k \in \mathbb{N}_\infty$ and any index $i \in \iota$, the function $\text{Pi.single } i : F'_i \to \prod_{i \in \iota} F'_i$ is $C^k$-differentiable. Here, $\text{Pi.single } i$ denotes the function that maps a value $v \in F'_i$ to the element of $\prod_{i \in \iota} F'_i$ which is $v$ at index $i$ and zero elsewhere.

contDiff_apply theorem

(i : ι) : ContDiff 𝕜 n fun f : ι → E => f i

Full source

theorem contDiff_apply (i : ι) : ContDiff 𝕜 n fun f : ι → E => f i :=
  contDiff_pi.mp contDiff_id i

$C^n$-Differentiability of Evaluation Maps

Informal description

For any index $i$ in a finite index set $\iota$, the evaluation map $f \mapsto f(i)$ from the space of functions $\iota \to E$ to $E$ is $C^n$-differentiable (continuously differentiable of order $n$) over the field $\mathbb{K}$.

contDiff_apply_apply theorem

(i : ι) (j : ι') : ContDiff 𝕜 n fun f : ι → ι' → E => f i j

Full source

theorem contDiff_apply_apply (i : ι) (j : ι') : ContDiff 𝕜 n fun f : ι → ι' → E => f i j :=
  contDiff_pi.mp (contDiff_apply 𝕜 (ι' → E) i) j

$C^n$-Differentiability of Double Evaluation Maps

Informal description

For any indices $i \in \iota$ and $j \in \iota'$, the evaluation map $f \mapsto f(i)(j)$ from the space of functions $\iota \to \iota' \to E$ to $E$ is $C^n$-differentiable (continuously differentiable of order $n$) over the field $\mathbb{K}$.

HasFTaylorSeriesUpToOn.add theorem

 {n : WithTop ℕ∞} {q g} (hf : HasFTaylorSeriesUpToOn n f p s) (hg : HasFTaylorSeriesUpToOn n g q s) :
  HasFTaylorSeriesUpToOn n (f + g) (p + q) s

Full source

theorem HasFTaylorSeriesUpToOn.add {n : WithTop ℕ∞} {q g} (hf : HasFTaylorSeriesUpToOn n f p s)
    (hg : HasFTaylorSeriesUpToOn n g q s) : HasFTaylorSeriesUpToOn n (f + g) (p + q) s := by
  exact HasFTaylorSeriesUpToOn.continuousLinearMap_comp
    (ContinuousLinearMap.fst 𝕜 F F + .snd 𝕜 F F) (hf.prodMk hg)

Taylor Series Expansion of Sum of Functions up to Order $n$

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $s \subseteq E$ be a subset. Suppose $f$ and $g$ are functions from $E$ to $F$ with Taylor series expansions $p$ and $q$ up to order $n$ on $s$, respectively. Then the sum $f + g$ has a Taylor series expansion up to order $n$ on $s$ given by $p + q$.

contDiff_add theorem

: ContDiff 𝕜 n fun p : F × F => p.1 + p.2

Full source

theorem contDiff_add : ContDiff 𝕜 n fun p : F × F => p.1 + p.2 :=
  (IsBoundedLinearMap.fst.add IsBoundedLinearMap.snd).contDiff

$C^n$ Differentiability of Addition in Normed Spaces

Informal description

Let $F$ be a normed space over a nontrivially normed field $\mathbb{K}$. The addition operation $(x, y) \mapsto x + y$ on $F \times F$ is continuously differentiable of order $n$ (i.e., $C^n$) for any extended natural number $n \in \mathbb{N}_\infty$.

ContDiffWithinAt.add theorem

 {s : Set E} {f g : E → F} (hf : ContDiffWithinAt 𝕜 n f s x) (hg : ContDiffWithinAt 𝕜 n g s x) :
  ContDiffWithinAt 𝕜 n (fun x => f x + g x) s x

Full source

/-- The sum of two `C^n` functions within a set at a point is `C^n` within this set
at this point. -/
theorem ContDiffWithinAt.add {s : Set E} {f g : E → F} (hf : ContDiffWithinAt 𝕜 n f s x)
    (hg : ContDiffWithinAt 𝕜 n g s x) : ContDiffWithinAt 𝕜 n (fun x => f x + g x) s x :=
  contDiff_add.contDiffWithinAt.comp x (hf.prodMk hg) subset_preimage_univ

Sum of $C^n$ functions within a set at a point is $C^n$

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $s \subseteq E$ be a subset. For any extended natural number $n \in \mathbb{N}_\infty$ and point $x \in E$, if $f, g : E \to F$ are $C^n$ functions within $s$ at $x$, then their sum $x \mapsto f(x) + g(x)$ is also $C^n$ within $s$ at $x$.

ContDiffAt.add theorem

{f g : E → F} (hf : ContDiffAt 𝕜 n f x) (hg : ContDiffAt 𝕜 n g x) : ContDiffAt 𝕜 n (fun x => f x + g x) x

Full source

/-- The sum of two `C^n` functions at a point is `C^n` at this point. -/
theorem ContDiffAt.add {f g : E → F} (hf : ContDiffAt 𝕜 n f x) (hg : ContDiffAt 𝕜 n g x) :
    ContDiffAt 𝕜 n (fun x => f x + g x) x := by
  rw [← contDiffWithinAt_univ] at *; exact hf.add hg

Sum of $C^n$ functions at a point is $C^n$

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $n \in \mathbb{N}_\infty$. For any point $x \in E$, if $f, g : E \to F$ are $C^n$ functions at $x$, then their sum $x \mapsto f(x) + g(x)$ is also $C^n$ at $x$.

ContDiff.add theorem

{f g : E → F} (hf : ContDiff 𝕜 n f) (hg : ContDiff 𝕜 n g) : ContDiff 𝕜 n fun x => f x + g x

Full source

/-- The sum of two `C^n`functions is `C^n`. -/
theorem ContDiff.add {f g : E → F} (hf : ContDiff 𝕜 n f) (hg : ContDiff 𝕜 n g) :
    ContDiff 𝕜 n fun x => f x + g x :=
  contDiff_add.comp (hf.prodMk hg)

Sum of $C^n$ functions is $C^n$

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $n \in \mathbb{N}_\infty$. If $f, g : E \to F$ are $C^n$ functions, then their sum $x \mapsto f(x) + g(x)$ is also $C^n$.

ContDiffOn.add theorem

 {s : Set E} {f g : E → F} (hf : ContDiffOn 𝕜 n f s) (hg : ContDiffOn 𝕜 n g s) : ContDiffOn 𝕜 n (fun x => f x + g x) s

Full source

/-- The sum of two `C^n` functions on a domain is `C^n`. -/
theorem ContDiffOn.add {s : Set E} {f g : E → F} (hf : ContDiffOn 𝕜 n f s)
    (hg : ContDiffOn 𝕜 n g s) : ContDiffOn 𝕜 n (fun x => f x + g x) s := fun x hx =>
  (hf x hx).add (hg x hx)

Sum of $C^n$ functions on a set is $C^n$

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $s \subseteq E$ be a subset. For any extended natural number $n \in \mathbb{N}_\infty$, if $f, g : E \to F$ are $C^n$ functions on $s$, then their sum $x \mapsto f(x) + g(x)$ is also $C^n$ on $s$.

iteratedFDerivWithin_add_apply theorem

 {f g : E → F} (hf : ContDiffWithinAt 𝕜 i f s x) (hg : ContDiffWithinAt 𝕜 i g s x) (hu : UniqueDiffOn 𝕜 s)
  (hx : x ∈ s) : iteratedFDerivWithin 𝕜 i (f + g) s x = iteratedFDerivWithin 𝕜 i f s x + iteratedFDerivWithin 𝕜 i g s x

Full source

/-- The iterated derivative of the sum of two functions is the sum of the iterated derivatives.
See also `iteratedFDerivWithin_add_apply'`, which uses the spelling `(fun x ↦ f x + g x)`
instead of `f + g`. -/
theorem iteratedFDerivWithin_add_apply {f g : E → F} (hf : ContDiffWithinAt 𝕜 i f s x)
    (hg : ContDiffWithinAt 𝕜 i g s x) (hu : UniqueDiffOn 𝕜 s) (hx : x ∈ s) :
    iteratedFDerivWithin 𝕜 i (f + g) s x =
      iteratedFDerivWithin 𝕜 i f s x + iteratedFDerivWithin 𝕜 i g s x := by
  have := (hf.eventually (by simp)).and (hg.eventually (by simp))
  obtain ⟨t, ht, hxt, h⟩ := mem_nhdsWithin.mp this
  have hft : ContDiffOn 𝕜 i f (s ∩ t) := fun a ha ↦ (h (by simp_all)).1.mono inter_subset_left
  have hgt : ContDiffOn 𝕜 i g (s ∩ t) := fun a ha ↦ (h (by simp_all)).2.mono inter_subset_left
  have hut : UniqueDiffOn 𝕜 (s ∩ t) := hu.inter ht
  have H : ↑(s ∩ t) =ᶠ[𝓝 x] s :=
    inter_eventuallyEq_left.mpr (eventually_of_mem (ht.mem_nhds hxt) (fun _ h _ ↦ h))
  rw [← iteratedFDerivWithin_congr_set H, ← iteratedFDerivWithin_congr_set H,
    ← iteratedFDerivWithin_congr_set H]
  exact .symm (((hft.ftaylorSeriesWithin hut).add
      (hgt.ftaylorSeriesWithin hut)).eq_iteratedFDerivWithin_of_uniqueDiffOn le_rfl hut ⟨hx, hxt⟩)

Linearity of Iterated Fréchet Derivative for Sum of Functions

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $s \subseteq E$ be a set with unique differentiability. For functions $f, g : E \to F$ that are $C^i$ within $s$ at a point $x \in s$, the $i$-th iterated Fréchet derivative of $f + g$ within $s$ at $x$ equals the sum of the $i$-th iterated Fréchet derivatives of $f$ and $g$ within $s$ at $x$: \[ D^i(f + g)(x) = D^i f(x) + D^i g(x). \]

iteratedFDerivWithin_add_apply' theorem

 {f g : E → F} (hf : ContDiffWithinAt 𝕜 i f s x) (hg : ContDiffWithinAt 𝕜 i g s x) (hu : UniqueDiffOn 𝕜 s)
  (hx : x ∈ s) :
  iteratedFDerivWithin 𝕜 i (fun x => f x + g x) s x = iteratedFDerivWithin 𝕜 i f s x + iteratedFDerivWithin 𝕜 i g s x

Full source

/-- The iterated derivative of the sum of two functions is the sum of the iterated derivatives.
This is the same as `iteratedFDerivWithin_add_apply`, but using the spelling `(fun x ↦ f x + g x)`
instead of `f + g`, which can be handy for some rewrites.
TODO: use one form consistently. -/
theorem iteratedFDerivWithin_add_apply' {f g : E → F} (hf : ContDiffWithinAt 𝕜 i f s x)
    (hg : ContDiffWithinAt 𝕜 i g s x) (hu : UniqueDiffOn 𝕜 s) (hx : x ∈ s) :
    iteratedFDerivWithin 𝕜 i (fun x => f x + g x) s x =
      iteratedFDerivWithin 𝕜 i f s x + iteratedFDerivWithin 𝕜 i g s x :=
  iteratedFDerivWithin_add_apply hf hg hu hx

Linearity of Iterated Fréchet Derivative for Pointwise Sum of Functions

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $s \subseteq E$ be a set with unique differentiability. For functions $f, g : E \to F$ that are $C^i$ within $s$ at a point $x \in s$, the $i$-th iterated Fréchet derivative of the sum $x \mapsto f(x) + g(x)$ within $s$ at $x$ equals the sum of the $i$-th iterated Fréchet derivatives of $f$ and $g$ within $s$ at $x$: \[ D^i(f + g)(x) = D^i f(x) + D^i g(x). \]

iteratedFDeriv_add_apply theorem

 {i : ℕ} {f g : E → F} (hf : ContDiffAt 𝕜 i f x) (hg : ContDiffAt 𝕜 i g x) :
  iteratedFDeriv 𝕜 i (f + g) x = iteratedFDeriv 𝕜 i f x + iteratedFDeriv 𝕜 i g x

Full source

theorem iteratedFDeriv_add_apply {i : ℕ} {f g : E → F}
    (hf : ContDiffAt 𝕜 i f x) (hg : ContDiffAt 𝕜 i g x) :
    iteratedFDeriv 𝕜 i (f + g) x = iteratedFDeriv 𝕜 i f x + iteratedFDeriv 𝕜 i g x := by
  simp_rw [← iteratedFDerivWithin_univ]
  exact iteratedFDerivWithin_add_apply hf hg uniqueDiffOn_univ (Set.mem_univ _)

Linearity of Iterated Fréchet Derivative for Sum of Functions at a Point

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$. For functions $f, g : E \to F$ that are $C^i$ at a point $x \in E$, the $i$-th iterated Fréchet derivative of $f + g$ at $x$ equals the sum of the $i$-th iterated Fréchet derivatives of $f$ and $g$ at $x$: \[ D^i(f + g)(x) = D^i f(x) + D^i g(x). \]

iteratedFDeriv_add_apply' theorem

 {i : ℕ} {f g : E → F} (hf : ContDiffAt 𝕜 i f x) (hg : ContDiffAt 𝕜 i g x) :
  iteratedFDeriv 𝕜 i (fun x => f x + g x) x = iteratedFDeriv 𝕜 i f x + iteratedFDeriv 𝕜 i g x

Full source

theorem iteratedFDeriv_add_apply' {i : ℕ} {f g : E → F} (hf : ContDiffAt 𝕜 i f x)
    (hg : ContDiffAt 𝕜 i g x) :
    iteratedFDeriv 𝕜 i (fun x => f x + g x) x = iteratedFDeriv 𝕜 i f x + iteratedFDeriv 𝕜 i g x :=
  iteratedFDeriv_add_apply hf hg

Linearity of Iterated Fréchet Derivative for Pointwise Sum of Functions at a Point

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$. For functions $f, g : E \to F$ that are $C^i$ at a point $x \in E$, the $i$-th iterated Fréchet derivative of the sum $x \mapsto f(x) + g(x)$ at $x$ equals the sum of the $i$-th iterated Fréchet derivatives of $f$ and $g$ at $x$: \[ D^i(f + g)(x) = D^i f(x) + D^i g(x). \]

contDiff_neg theorem

: ContDiff 𝕜 n fun p : F => -p

Full source

theorem contDiff_neg : ContDiff 𝕜 n fun p : F => -p :=
  IsBoundedLinearMap.id.neg.contDiff

Negation is $C^n$ on a normed space

Informal description

Let $F$ be a normed vector space over a nontrivially normed field $\mathbb{K}$. The negation operation $p \mapsto -p$ is $C^n$ (continuously differentiable of order $n$) as a function from $F$ to itself, for any extended natural number $n \in \mathbb{N}_\infty$.

ContDiffWithinAt.neg theorem

{s : Set E} {f : E → F} (hf : ContDiffWithinAt 𝕜 n f s x) : ContDiffWithinAt 𝕜 n (fun x => -f x) s x

Full source

/-- The negative of a `C^n` function within a domain at a point is `C^n` within this domain at
this point. -/
theorem ContDiffWithinAt.neg {s : Set E} {f : E → F} (hf : ContDiffWithinAt 𝕜 n f s x) :
    ContDiffWithinAt 𝕜 n (fun x => -f x) s x :=
  contDiff_neg.contDiffWithinAt.comp x hf subset_preimage_univ

Negation preserves $C^n$ differentiability within a set at a point

Informal description

Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function. If $f$ is $C^n$ (continuously differentiable of order $n$) within a set $s \subseteq E$ at a point $x \in E$, then the function $x \mapsto -f(x)$ is also $C^n$ within $s$ at $x$.

ContDiffAt.neg theorem

{f : E → F} (hf : ContDiffAt 𝕜 n f x) : ContDiffAt 𝕜 n (fun x => -f x) x

Full source

/-- The negative of a `C^n` function at a point is `C^n` at this point. -/
theorem ContDiffAt.neg {f : E → F} (hf : ContDiffAt 𝕜 n f x) :
    ContDiffAt 𝕜 n (fun x => -f x) x := by rw [← contDiffWithinAt_univ] at *; exact hf.neg

Negation preserves $C^n$ differentiability at a point

Informal description

Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function. If $f$ is $C^n$ (continuously differentiable of order $n$) at a point $x \in E$, then the function $x \mapsto -f(x)$ is also $C^n$ at $x$.

ContDiff.neg theorem

{f : E → F} (hf : ContDiff 𝕜 n f) : ContDiff 𝕜 n fun x => -f x

Full source

/-- The negative of a `C^n`function is `C^n`. -/
theorem ContDiff.neg {f : E → F} (hf : ContDiff 𝕜 n f) : ContDiff 𝕜 n fun x => -f x :=
  contDiff_neg.comp hf

Negation preserves $C^n$ differentiability

Informal description

Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a $C^n$ function (continuously differentiable of order $n$) for some $n \in \mathbb{N}_\infty$. Then the function $x \mapsto -f(x)$ is also $C^n$.

ContDiffOn.neg theorem

{s : Set E} {f : E → F} (hf : ContDiffOn 𝕜 n f s) : ContDiffOn 𝕜 n (fun x => -f x) s

Full source

/-- The negative of a `C^n` function on a domain is `C^n`. -/
theorem ContDiffOn.neg {s : Set E} {f : E → F} (hf : ContDiffOn 𝕜 n f s) :
    ContDiffOn 𝕜 n (fun x => -f x) s := fun x hx => (hf x hx).neg

Negation preserves $C^n$ differentiability on a set

Informal description

Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function. If $f$ is $C^n$ (continuously differentiable of order $n$) on a set $s \subseteq E$, then the function $x \mapsto -f(x)$ is also $C^n$ on $s$.

iteratedFDerivWithin_neg_apply theorem

 {f : E → F} (hu : UniqueDiffOn 𝕜 s) (hx : x ∈ s) : iteratedFDerivWithin 𝕜 i (-f) s x = -iteratedFDerivWithin 𝕜 i f s x

Full source

theorem iteratedFDerivWithin_neg_apply {f : E → F} (hu : UniqueDiffOn 𝕜 s) (hx : x ∈ s) :
    iteratedFDerivWithin 𝕜 i (-f) s x = -iteratedFDerivWithin 𝕜 i f s x := by
  induction' i with i hi generalizing x
  · ext; simp
  · ext h
    calc
      iteratedFDerivWithin 𝕜 (i + 1) (-f) s x h =
          fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i (-f) s) s x (h 0) (Fin.tail h) :=
        rfl
      _ = fderivWithin 𝕜 (-iteratedFDerivWithin 𝕜 i f s) s x (h 0) (Fin.tail h) := by
        rw [fderivWithin_congr' (@hi) hx]; rfl
      _ = -(fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i f s) s) x (h 0) (Fin.tail h) := by
        rw [Pi.neg_def, fderivWithin_neg (hu x hx)]; rfl
      _ = -(iteratedFDerivWithin 𝕜 (i + 1) f s) x h := rfl

Iterated Fréchet Derivative of Negated Function Equals Negation of Iterated Fréchet Derivative

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function. For any set $s \subseteq E$ where $\mathbb{K}$-differentiation is uniquely defined on $s$ (i.e., $\text{UniqueDiffOn}\ \mathbb{K}\ s$ holds), and for any point $x \in s$, the $i$-th iterated Fréchet derivative within $s$ of the function $-f$ at $x$ equals the negation of the $i$-th iterated Fréchet derivative within $s$ of $f$ at $x$. That is, \[ \text{iteratedFDerivWithin}\ \mathbb{K}\ i\ (-f)\ s\ x = -\text{iteratedFDerivWithin}\ \mathbb{K}\ i\ f\ s\ x. \]

iteratedFDeriv_neg_apply theorem

{i : ℕ} {f : E → F} : iteratedFDeriv 𝕜 i (-f) x = -iteratedFDeriv 𝕜 i f x

Full source

theorem iteratedFDeriv_neg_apply {i : ℕ} {f : E → F} :
    iteratedFDeriv 𝕜 i (-f) x = -iteratedFDeriv 𝕜 i f x := by
  simp_rw [← iteratedFDerivWithin_univ]
  exact iteratedFDerivWithin_neg_apply uniqueDiffOn_univ (Set.mem_univ _)

Iterated Fréchet derivative of negation equals negation of iterated Fréchet derivative

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function. For any $i \in \mathbb{N}$ and any point $x \in E$, the $i$-th iterated Fréchet derivative of the function $-f$ at $x$ equals the negation of the $i$-th iterated Fréchet derivative of $f$ at $x$. That is, \[ D^i(-f)(x) = -D^i f(x). \]

ContDiffWithinAt.sub theorem

 {s : Set E} {f g : E → F} (hf : ContDiffWithinAt 𝕜 n f s x) (hg : ContDiffWithinAt 𝕜 n g s x) :
  ContDiffWithinAt 𝕜 n (fun x => f x - g x) s x

Full source

/-- The difference of two `C^n` functions within a set at a point is `C^n` within this set
at this point. -/
theorem ContDiffWithinAt.sub {s : Set E} {f g : E → F} (hf : ContDiffWithinAt 𝕜 n f s x)
    (hg : ContDiffWithinAt 𝕜 n g s x) : ContDiffWithinAt 𝕜 n (fun x => f x - g x) s x := by
  simpa only [sub_eq_add_neg] using hf.add hg.neg

Difference of $C^n$ functions within a set at a point is $C^n$

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $s \subseteq E$ be a subset. For any extended natural number $n \in \mathbb{N}_\infty$ and point $x \in E$, if $f, g : E \to F$ are $C^n$ functions within $s$ at $x$, then their difference $x \mapsto f(x) - g(x)$ is also $C^n$ within $s$ at $x$.

ContDiffAt.sub theorem

{f g : E → F} (hf : ContDiffAt 𝕜 n f x) (hg : ContDiffAt 𝕜 n g x) : ContDiffAt 𝕜 n (fun x => f x - g x) x

Full source

/-- The difference of two `C^n` functions at a point is `C^n` at this point. -/
theorem ContDiffAt.sub {f g : E → F} (hf : ContDiffAt 𝕜 n f x) (hg : ContDiffAt 𝕜 n g x) :
    ContDiffAt 𝕜 n (fun x => f x - g x) x := by simpa only [sub_eq_add_neg] using hf.add hg.neg

Difference of $C^n$ functions at a point is $C^n$

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $n \in \mathbb{N}_\infty$. For any point $x \in E$, if $f, g : E \to F$ are $C^n$ functions at $x$, then their difference $x \mapsto f(x) - g(x)$ is also $C^n$ at $x$.

ContDiffOn.sub theorem

 {s : Set E} {f g : E → F} (hf : ContDiffOn 𝕜 n f s) (hg : ContDiffOn 𝕜 n g s) : ContDiffOn 𝕜 n (fun x => f x - g x) s

Full source

/-- The difference of two `C^n` functions on a domain is `C^n`. -/
theorem ContDiffOn.sub {s : Set E} {f g : E → F} (hf : ContDiffOn 𝕜 n f s)
    (hg : ContDiffOn 𝕜 n g s) : ContDiffOn 𝕜 n (fun x => f x - g x) s := by
  simpa only [sub_eq_add_neg] using hf.add hg.neg

Difference of $C^n$ functions on a set is $C^n$

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $s \subseteq E$ be a subset. For any extended natural number $n \in \mathbb{N}_\infty$, if $f, g : E \to F$ are $C^n$ functions on $s$, then their difference $x \mapsto f(x) - g(x)$ is also $C^n$ on $s$.

ContDiff.sub theorem

{f g : E → F} (hf : ContDiff 𝕜 n f) (hg : ContDiff 𝕜 n g) : ContDiff 𝕜 n fun x => f x - g x

Full source

/-- The difference of two `C^n` functions is `C^n`. -/
theorem ContDiff.sub {f g : E → F} (hf : ContDiff 𝕜 n f) (hg : ContDiff 𝕜 n g) :
    ContDiff 𝕜 n fun x => f x - g x := by simpa only [sub_eq_add_neg] using hf.add hg.neg

Difference of $C^n$ functions is $C^n$

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $n \in \mathbb{N}_\infty$. If $f, g : E \to F$ are $C^n$ functions (continuously differentiable of order $n$), then their difference $x \mapsto f(x) - g(x)$ is also $C^n$.

ContDiffWithinAt.sum theorem

 {ι : Type*} {f : ι → E → F} {s : Finset ι} {t : Set E} {x : E}
  (h : ∀ i ∈ s, ContDiffWithinAt 𝕜 n (fun x => f i x) t x) : ContDiffWithinAt 𝕜 n (fun x => ∑ i ∈ s, f i x) t x

Full source

theorem ContDiffWithinAt.sum {ι : Type*} {f : ι → E → F} {s : Finset ι} {t : Set E} {x : E}
    (h : ∀ i ∈ s, ContDiffWithinAt 𝕜 n (fun x => f i x) t x) :
    ContDiffWithinAt 𝕜 n (fun x => ∑ i ∈ s, f i x) t x := by
  classical
    induction' s using Finset.induction_on with i s is IH
    · simp [contDiffWithinAt_const]
    · simp only [is, Finset.sum_insert, not_false_iff]
      exact (h _ (Finset.mem_insert_self i s)).add
        (IH fun j hj => h _ (Finset.mem_insert_of_mem hj))

Finite Sum of $C^n$ Functions is $C^n$ Within a Set at a Point

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, let $t \subseteq E$ be a subset, and let $x \in E$. For any finite index set $\iota$, functions $f_i : E \to F$ for $i \in \iota$, and extended natural number $n \in \mathbb{N}_\infty$, if each $f_i$ is $C^n$ within $t$ at $x$, then their finite sum $\sum_{i \in \iota} f_i$ is also $C^n$ within $t$ at $x$.

ContDiffAt.sum theorem

 {ι : Type*} {f : ι → E → F} {s : Finset ι} {x : E} (h : ∀ i ∈ s, ContDiffAt 𝕜 n (fun x => f i x) x) :
  ContDiffAt 𝕜 n (fun x => ∑ i ∈ s, f i x) x

Full source

theorem ContDiffAt.sum {ι : Type*} {f : ι → E → F} {s : Finset ι} {x : E}
    (h : ∀ i ∈ s, ContDiffAt 𝕜 n (fun x => f i x) x) :
    ContDiffAt 𝕜 n (fun x => ∑ i ∈ s, f i x) x := by
  rw [← contDiffWithinAt_univ] at *; exact ContDiffWithinAt.sum h

Finite Sum of $C^n$ Functions is $C^n$ at a Point

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $n \in \mathbb{N}_\infty$. Given a finite index set $\iota$, functions $f_i : E \to F$ for $i \in \iota$, and a point $x \in E$, if each $f_i$ is $C^n$ at $x$, then their finite sum $\sum_{i \in \iota} f_i$ is also $C^n$ at $x$.

ContDiffOn.sum theorem

 {ι : Type*} {f : ι → E → F} {s : Finset ι} {t : Set E} (h : ∀ i ∈ s, ContDiffOn 𝕜 n (fun x => f i x) t) :
  ContDiffOn 𝕜 n (fun x => ∑ i ∈ s, f i x) t

Full source

theorem ContDiffOn.sum {ι : Type*} {f : ι → E → F} {s : Finset ι} {t : Set E}
    (h : ∀ i ∈ s, ContDiffOn 𝕜 n (fun x => f i x) t) :
    ContDiffOn 𝕜 n (fun x => ∑ i ∈ s, f i x) t := fun x hx =>
  ContDiffWithinAt.sum fun i hi => h i hi x hx

Sum of $C^n$ Functions is $C^n$ on a Set

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $t \subseteq E$ be a subset. For any finite index set $\iota$, functions $f_i : E \to F$ for $i \in \iota$, and extended natural number $n \in \mathbb{N}_\infty$, if each $f_i$ is $C^n$ on $t$, then their finite sum $\sum_{i \in \iota} f_i$ is also $C^n$ on $t$.

ContDiff.sum theorem

 {ι : Type*} {f : ι → E → F} {s : Finset ι} (h : ∀ i ∈ s, ContDiff 𝕜 n fun x => f i x) :
  ContDiff 𝕜 n fun x => ∑ i ∈ s, f i x

Full source

theorem ContDiff.sum {ι : Type*} {f : ι → E → F} {s : Finset ι}
    (h : ∀ i ∈ s, ContDiff 𝕜 n fun x => f i x) : ContDiff 𝕜 n fun x => ∑ i ∈ s, f i x := by
  simp only [← contDiffOn_univ] at *; exact ContDiffOn.sum h

Sum of $C^n$ Functions is $C^n$

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $n \in \mathbb{N}_\infty$. Given a finite index set $\iota$ and functions $f_i : E \to F$ for $i \in \iota$, if each $f_i$ is $C^n$ (continuously differentiable of order $n$), then their finite sum $\sum_{i \in \iota} f_i$ is also $C^n$.

iteratedFDerivWithin_sum_apply theorem

 {ι : Type*} {f : ι → E → F} {u : Finset ι} {i : ℕ} {x : E} (hs : UniqueDiffOn 𝕜 s) (hx : x ∈ s)
  (h : ∀ j ∈ u, ContDiffWithinAt 𝕜 i (f j) s x) :
  iteratedFDerivWithin 𝕜 i (∑ j ∈ u, f j ·) s x = ∑ j ∈ u, iteratedFDerivWithin 𝕜 i (f j) s x

Full source

theorem iteratedFDerivWithin_sum_apply {ι : Type*} {f : ι → E → F} {u : Finset ι} {i : ℕ} {x : E}
    (hs : UniqueDiffOn 𝕜 s) (hx : x ∈ s) (h : ∀ j ∈ u, ContDiffWithinAt 𝕜 i (f j) s x) :
    iteratedFDerivWithin 𝕜 i (∑ j ∈ u, f j ·) s x =
      ∑ j ∈ u, iteratedFDerivWithin 𝕜 i (f j) s x := by
  induction u using Finset.cons_induction with
  | empty => ext; simp [hs, hx]
  | cons a u ha IH =>
    simp only [Finset.mem_cons, forall_eq_or_imp] at h
    simp only [Finset.sum_cons]
    rw [iteratedFDerivWithin_add_apply' h.1 (ContDiffWithinAt.sum h.2) hs hx, IH h.2]

Linearity of Iterated Fréchet Derivative for Finite Sums within a Set

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $s \subseteq E$ be a set with unique differentiability. For a finite index set $\iota$, functions $f_j : E \to F$ for $j \in \iota$, a natural number $i$, and a point $x \in s$, if each $f_j$ is $C^i$ within $s$ at $x$, then the $i$-th iterated Fréchet derivative of the sum $\sum_{j \in \iota} f_j$ within $s$ at $x$ equals the sum of the $i$-th iterated Fréchet derivatives of the $f_j$ within $s$ at $x$: \[ D^i\left(\sum_{j \in \iota} f_j\right)(x) = \sum_{j \in \iota} D^i f_j(x). \]

iteratedFDeriv_sum theorem

 {ι : Type*} {f : ι → E → F} {u : Finset ι} {i : ℕ} (h : ∀ j ∈ u, ContDiff 𝕜 i (f j)) :
  iteratedFDeriv 𝕜 i (∑ j ∈ u, f j ·) = ∑ j ∈ u, iteratedFDeriv 𝕜 i (f j)

Full source

theorem iteratedFDeriv_sum {ι : Type*} {f : ι → E → F} {u : Finset ι} {i : ℕ}
    (h : ∀ j ∈ u, ContDiff 𝕜 i (f j)) :
    iteratedFDeriv 𝕜 i (∑ j ∈ u, f j ·) = ∑ j ∈ u, iteratedFDeriv 𝕜 i (f j) :=
  funext fun x ↦ by simpa [iteratedFDerivWithin_univ] using
    iteratedFDerivWithin_sum_apply uniqueDiffOn_univ (mem_univ x) (h · · |>.contDiffWithinAt)

Linearity of Iterated Fréchet Derivative for Finite Sums of $C^n$ Functions

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $n \in \mathbb{N}_\infty$. Given a finite index set $\iota$ and functions $f_j : E \to F$ for $j \in \iota$, if each $f_j$ is $C^n$ (continuously differentiable of order $n$), then the $n$-th iterated Fréchet derivative of the finite sum $\sum_{j \in \iota} f_j$ equals the sum of the $n$-th iterated Fréchet derivatives of the $f_j$: \[ D^n\left(\sum_{j \in \iota} f_j\right) = \sum_{j \in \iota} D^n f_j. \]

contDiff_mul theorem

: ContDiff 𝕜 n fun p : 𝔸 × 𝔸 => p.1 * p.2

Full source

theorem contDiff_mul : ContDiff 𝕜 n fun p : 𝔸 × 𝔸 => p.1 * p.2 :=
  (ContinuousLinearMap.mul 𝕜 𝔸).isBoundedBilinearMap.contDiff

$C^n$-Differentiability of Multiplication in Normed Algebras

Informal description

Let $\mathbb{K}$ be a nontrivially normed field and $\mathfrak{A}$ be a normed algebra over $\mathbb{K}$. The multiplication operation $(x, y) \mapsto x \cdot y$ on $\mathfrak{A} \times \mathfrak{A}$ is $C^n$-differentiable for any extended natural number $n \in \mathbb{N}_\infty$.

ContDiffWithinAt.mul theorem

 {s : Set E} {f g : E → 𝔸} (hf : ContDiffWithinAt 𝕜 n f s x) (hg : ContDiffWithinAt 𝕜 n g s x) :
  ContDiffWithinAt 𝕜 n (fun x => f x * g x) s x

Full source

/-- The product of two `C^n` functions within a set at a point is `C^n` within this set
at this point. -/
theorem ContDiffWithinAt.mul {s : Set E} {f g : E → 𝔸} (hf : ContDiffWithinAt 𝕜 n f s x)
    (hg : ContDiffWithinAt 𝕜 n g s x) : ContDiffWithinAt 𝕜 n (fun x => f x * g x) s x :=
  contDiff_mul.comp_contDiffWithinAt (hf.prodMk hg)

$C^n$-Differentiability of Pointwise Product Within a Set at a Point

Informal description

Let $E$ be a normed space over a nontrivially normed field $\mathbb{K}$, $\mathfrak{A}$ be a normed algebra over $\mathbb{K}$, and $s \subseteq E$ be a subset. For two functions $f, g : E \to \mathfrak{A}$ that are $C^n$-differentiable within $s$ at a point $x \in E$, their pointwise product function $x \mapsto f(x) \cdot g(x)$ is also $C^n$-differentiable within $s$ at $x$.

ContDiffAt.mul theorem

{f g : E → 𝔸} (hf : ContDiffAt 𝕜 n f x) (hg : ContDiffAt 𝕜 n g x) : ContDiffAt 𝕜 n (fun x => f x * g x) x

Full source

/-- The product of two `C^n` functions at a point is `C^n` at this point. -/
nonrec theorem ContDiffAt.mul {f g : E → 𝔸} (hf : ContDiffAt 𝕜 n f x) (hg : ContDiffAt 𝕜 n g x) :
    ContDiffAt 𝕜 n (fun x => f x * g x) x :=
  hf.mul hg

$C^n$-Differentiability of Pointwise Product at a Point in Normed Algebras

Informal description

Let $E$ be a normed space over a nontrivially normed field $\mathbb{K}$, $\mathfrak{A}$ be a normed algebra over $\mathbb{K}$, and $x \in E$. For any two functions $f, g : E \to \mathfrak{A}$ that are $C^n$-differentiable at $x$, their pointwise product function $x \mapsto f(x) \cdot g(x)$ is also $C^n$-differentiable at $x$.

ContDiffOn.mul theorem

{f g : E → 𝔸} (hf : ContDiffOn 𝕜 n f s) (hg : ContDiffOn 𝕜 n g s) : ContDiffOn 𝕜 n (fun x => f x * g x) s

Full source

/-- The product of two `C^n` functions on a domain is `C^n`. -/
theorem ContDiffOn.mul {f g : E → 𝔸} (hf : ContDiffOn 𝕜 n f s) (hg : ContDiffOn 𝕜 n g s) :
    ContDiffOn 𝕜 n (fun x => f x * g x) s := fun x hx => (hf x hx).mul (hg x hx)

Product of $C^n$-Differentiable Functions is $C^n$-Differentiable on a Set

Informal description

Let $E$ be a normed space over a nontrivially normed field $\mathbb{K}$, $\mathfrak{A}$ be a normed algebra over $\mathbb{K}$, and $s \subseteq E$ be a subset. For any two functions $f, g : E \to \mathfrak{A}$ that are $C^n$-differentiable on $s$, their pointwise product function $x \mapsto f(x) \cdot g(x)$ is also $C^n$-differentiable on $s$.

ContDiff.mul theorem

{f g : E → 𝔸} (hf : ContDiff 𝕜 n f) (hg : ContDiff 𝕜 n g) : ContDiff 𝕜 n fun x => f x * g x

Full source

/-- The product of two `C^n`functions is `C^n`. -/
theorem ContDiff.mul {f g : E → 𝔸} (hf : ContDiff 𝕜 n f) (hg : ContDiff 𝕜 n g) :
    ContDiff 𝕜 n fun x => f x * g x :=
  contDiff_mul.comp (hf.prodMk hg)

$C^n$-Differentiability of Pointwise Product of Functions in Normed Algebras

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $E$ be a normed space over $\mathbb{K}$, and $\mathfrak{A}$ be a normed algebra over $\mathbb{K}$. For any two functions $f, g : E \to \mathfrak{A}$ that are $C^n$-differentiable (continuously differentiable of order $n$) over $\mathbb{K}$, their pointwise product function $x \mapsto f(x) \cdot g(x)$ is also $C^n$-differentiable over $\mathbb{K}$.

contDiffWithinAt_prod' theorem

 {t : Finset ι} {f : ι → E → 𝔸'} (h : ∀ i ∈ t, ContDiffWithinAt 𝕜 n (f i) s x) : ContDiffWithinAt 𝕜 n (∏ i ∈ t, f i) s x

Full source

theorem contDiffWithinAt_prod' {t : Finset ι} {f : ι → E → 𝔸'}
    (h : ∀ i ∈ t, ContDiffWithinAt 𝕜 n (f i) s x) : ContDiffWithinAt 𝕜 n (∏ i ∈ t, f i) s x :=
  Finset.prod_induction f (fun f => ContDiffWithinAt 𝕜 n f s x) (fun _ _ => ContDiffWithinAt.mul)
    (contDiffWithinAt_const (c := 1)) h

$C^n$-Differentiability of Finite Product of Functions Within a Set at a Point

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $E$ be a normed space over $\mathbb{K}$, $\mathfrak{A}'$ be a normed algebra over $\mathbb{K}$, $s \subseteq E$ be a subset, and $x \in E$. Given a finite index set $t$ and a family of functions $f_i : E \to \mathfrak{A}'$ for $i \in t$, if each $f_i$ is $C^n$-differentiable within $s$ at $x$, then the product function $\prod_{i \in t} f_i$ is also $C^n$-differentiable within $s$ at $x$.

contDiffWithinAt_prod theorem

 {t : Finset ι} {f : ι → E → 𝔸'} (h : ∀ i ∈ t, ContDiffWithinAt 𝕜 n (f i) s x) :
  ContDiffWithinAt 𝕜 n (fun y => ∏ i ∈ t, f i y) s x

Full source

theorem contDiffWithinAt_prod {t : Finset ι} {f : ι → E → 𝔸'}
    (h : ∀ i ∈ t, ContDiffWithinAt 𝕜 n (f i) s x) :
    ContDiffWithinAt 𝕜 n (fun y => ∏ i ∈ t, f i y) s x := by
  simpa only [← Finset.prod_apply] using contDiffWithinAt_prod' h

$C^n$-Differentiability of Pointwise Finite Product of Functions Within a Set at a Point

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $E$ be a normed space over $\mathbb{K}$, $\mathfrak{A}'$ be a normed algebra over $\mathbb{K}$, $s \subseteq E$ be a subset, and $x \in E$. Given a finite index set $t$ and a family of functions $f_i : E \to \mathfrak{A}'$ for $i \in t$, if each $f_i$ is $C^n$-differentiable within $s$ at $x$, then the pointwise product function $y \mapsto \prod_{i \in t} f_i(y)$ is also $C^n$-differentiable within $s$ at $x$.

contDiffAt_prod' theorem

 {t : Finset ι} {f : ι → E → 𝔸'} (h : ∀ i ∈ t, ContDiffAt 𝕜 n (f i) x) : ContDiffAt 𝕜 n (∏ i ∈ t, f i) x

Full source

theorem contDiffAt_prod' {t : Finset ι} {f : ι → E → 𝔸'} (h : ∀ i ∈ t, ContDiffAt 𝕜 n (f i) x) :
    ContDiffAt 𝕜 n (∏ i ∈ t, f i) x :=
  contDiffWithinAt_prod' h

$C^n$-Differentiability of Finite Product of Functions at a Point

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $E$ be a normed space over $\mathbb{K}$, $\mathfrak{A}'$ be a normed algebra over $\mathbb{K}$, and $x \in E$. Given a finite index set $t$ and a family of functions $f_i : E \to \mathfrak{A}'$ for $i \in t$, if each $f_i$ is $C^n$-differentiable at $x$, then the product function $\prod_{i \in t} f_i$ is also $C^n$-differentiable at $x$.

contDiffAt_prod theorem

 {t : Finset ι} {f : ι → E → 𝔸'} (h : ∀ i ∈ t, ContDiffAt 𝕜 n (f i) x) : ContDiffAt 𝕜 n (fun y => ∏ i ∈ t, f i y) x

Full source

theorem contDiffAt_prod {t : Finset ι} {f : ι → E → 𝔸'} (h : ∀ i ∈ t, ContDiffAt 𝕜 n (f i) x) :
    ContDiffAt 𝕜 n (fun y => ∏ i ∈ t, f i y) x :=
  contDiffWithinAt_prod h

$C^n$-Differentiability of Pointwise Finite Product of Functions at a Point

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $E$ be a normed space over $\mathbb{K}$, $\mathfrak{A}'$ be a normed algebra over $\mathbb{K}$, and $x \in E$. Given a finite index set $t$ and a family of functions $f_i : E \to \mathfrak{A}'$ for $i \in t$, if each $f_i$ is $C^n$-differentiable at $x$, then the pointwise product function $y \mapsto \prod_{i \in t} f_i(y)$ is also $C^n$-differentiable at $x$.

contDiffOn_prod' theorem

 {t : Finset ι} {f : ι → E → 𝔸'} (h : ∀ i ∈ t, ContDiffOn 𝕜 n (f i) s) : ContDiffOn 𝕜 n (∏ i ∈ t, f i) s

Full source

theorem contDiffOn_prod' {t : Finset ι} {f : ι → E → 𝔸'} (h : ∀ i ∈ t, ContDiffOn 𝕜 n (f i) s) :
    ContDiffOn 𝕜 n (∏ i ∈ t, f i) s := fun x hx => contDiffWithinAt_prod' fun i hi => h i hi x hx

$C^n$-Differentiability of Finite Product of Functions on a Set

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $E$ be a normed space over $\mathbb{K}$, $\mathfrak{A}'$ be a normed algebra over $\mathbb{K}$, and $s \subseteq E$ be a subset. Given a finite index set $t$ and a family of functions $f_i : E \to \mathfrak{A}'$ for $i \in t$, if each $f_i$ is $C^n$-differentiable on $s$, then the product function $\prod_{i \in t} f_i$ is also $C^n$-differentiable on $s$.

contDiffOn_prod theorem

 {t : Finset ι} {f : ι → E → 𝔸'} (h : ∀ i ∈ t, ContDiffOn 𝕜 n (f i) s) : ContDiffOn 𝕜 n (fun y => ∏ i ∈ t, f i y) s

Full source

theorem contDiffOn_prod {t : Finset ι} {f : ι → E → 𝔸'} (h : ∀ i ∈ t, ContDiffOn 𝕜 n (f i) s) :
    ContDiffOn 𝕜 n (fun y => ∏ i ∈ t, f i y) s := fun x hx =>
  contDiffWithinAt_prod fun i hi => h i hi x hx

$C^n$-Differentiability of Finite Pointwise Product of Functions on a Set

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $E$ be a normed space over $\mathbb{K}$, $\mathfrak{A}'$ be a normed algebra over $\mathbb{K}$, and $s \subseteq E$ be a subset. Given a finite index set $t$ and a family of functions $f_i : E \to \mathfrak{A}'$ for $i \in t$, if each $f_i$ is $C^n$-differentiable on $s$, then the pointwise product function $y \mapsto \prod_{i \in t} f_i(y)$ is also $C^n$-differentiable on $s$.

contDiff_prod' theorem

{t : Finset ι} {f : ι → E → 𝔸'} (h : ∀ i ∈ t, ContDiff 𝕜 n (f i)) : ContDiff 𝕜 n (∏ i ∈ t, f i)

Full source

theorem contDiff_prod' {t : Finset ι} {f : ι → E → 𝔸'} (h : ∀ i ∈ t, ContDiff 𝕜 n (f i)) :
    ContDiff 𝕜 n (∏ i ∈ t, f i) :=
  contDiff_iff_contDiffAt.mpr fun _ => contDiffAt_prod' fun i hi => (h i hi).contDiffAt

$C^n$-Differentiability of Finite Pointwise Product of Functions

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $E$ be a normed space over $\mathbb{K}$, and $\mathfrak{A}'$ be a normed algebra over $\mathbb{K}$. Given a finite index set $t$ and a family of functions $f_i : E \to \mathfrak{A}'$ for $i \in t$, if each $f_i$ is $C^n$-differentiable (continuously differentiable of order $n$) over $\mathbb{K}$, then the pointwise product function $\prod_{i \in t} f_i$ is also $C^n$-differentiable over $\mathbb{K}$.

contDiff_prod theorem

 {t : Finset ι} {f : ι → E → 𝔸'} (h : ∀ i ∈ t, ContDiff 𝕜 n (f i)) : ContDiff 𝕜 n fun y => ∏ i ∈ t, f i y

Full source

theorem contDiff_prod {t : Finset ι} {f : ι → E → 𝔸'} (h : ∀ i ∈ t, ContDiff 𝕜 n (f i)) :
    ContDiff 𝕜 n fun y => ∏ i ∈ t, f i y :=
  contDiff_iff_contDiffAt.mpr fun _ => contDiffAt_prod fun i hi => (h i hi).contDiffAt

$C^n$-Differentiability of Finite Pointwise Product of Functions

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $E$ be a normed space over $\mathbb{K}$, and $\mathfrak{A}'$ be a normed algebra over $\mathbb{K}$. Given a finite index set $t$ and a family of functions $f_i : E \to \mathfrak{A}'$ for $i \in t$, if each $f_i$ is $C^n$-differentiable (continuously differentiable of order $n$) over $\mathbb{K}$, then the pointwise product function $y \mapsto \prod_{i \in t} f_i(y)$ is also $C^n$-differentiable over $\mathbb{K}$.

ContDiff.pow theorem

{f : E → 𝔸} (hf : ContDiff 𝕜 n f) : ∀ m : ℕ, ContDiff 𝕜 n fun x => f x ^ m

Full source

theorem ContDiff.pow {f : E → 𝔸} (hf : ContDiff 𝕜 n f) : ∀ m : ℕ, ContDiff 𝕜 n fun x => f x ^ m
  | 0 => by simpa using contDiff_const
  | m + 1 => by simpa [pow_succ] using (hf.pow m).mul hf

$C^n$-Differentiability of Powers of a Function in Normed Algebras

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $E$ be a normed space over $\mathbb{K}$, and $\mathfrak{A}$ be a normed algebra over $\mathbb{K}$. If a function $f : E \to \mathfrak{A}$ is $C^n$-differentiable (continuously differentiable of order $n$) over $\mathbb{K}$, then for any natural number $m$, the function $x \mapsto (f(x))^m$ is also $C^n$-differentiable over $\mathbb{K}$.

ContDiffWithinAt.pow theorem

{f : E → 𝔸} (hf : ContDiffWithinAt 𝕜 n f s x) (m : ℕ) : ContDiffWithinAt 𝕜 n (fun y => f y ^ m) s x

Full source

theorem ContDiffWithinAt.pow {f : E → 𝔸} (hf : ContDiffWithinAt 𝕜 n f s x) (m : ℕ) :
    ContDiffWithinAt 𝕜 n (fun y => f y ^ m) s x :=
  (contDiff_id.pow m).comp_contDiffWithinAt hf

$C^n$-Differentiability of Powers within a Set at a Point

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $E$ be a normed space over $\mathbb{K}$, and $\mathfrak{A}$ be a normed algebra over $\mathbb{K}$. Given a function $f : E \to \mathfrak{A}$ that is $C^n$-differentiable within a set $s \subseteq E$ at a point $x \in E$, then for any natural number $m$, the function $y \mapsto (f(y))^m$ is also $C^n$-differentiable within $s$ at $x$.

ContDiffAt.pow theorem

{f : E → 𝔸} (hf : ContDiffAt 𝕜 n f x) (m : ℕ) : ContDiffAt 𝕜 n (fun y => f y ^ m) x

Full source

nonrec theorem ContDiffAt.pow {f : E → 𝔸} (hf : ContDiffAt 𝕜 n f x) (m : ℕ) :
    ContDiffAt 𝕜 n (fun y => f y ^ m) x :=
  hf.pow m

$C^n$-Differentiability of Powers at a Point in Normed Algebras

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $E$ be a normed space over $\mathbb{K}$, and $\mathfrak{A}$ be a normed algebra over $\mathbb{K}$. If a function $f : E \to \mathfrak{A}$ is $C^n$-differentiable at a point $x \in E$, then for any natural number $m$, the function $y \mapsto (f(y))^m$ is also $C^n$-differentiable at $x$.

ContDiffOn.pow theorem

{f : E → 𝔸} (hf : ContDiffOn 𝕜 n f s) (m : ℕ) : ContDiffOn 𝕜 n (fun y => f y ^ m) s

Full source

theorem ContDiffOn.pow {f : E → 𝔸} (hf : ContDiffOn 𝕜 n f s) (m : ℕ) :
    ContDiffOn 𝕜 n (fun y => f y ^ m) s := fun y hy => (hf y hy).pow m

$C^n$-Differentiability of Powers on a Set

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $E$ be a normed space over $\mathbb{K}$, and $\mathfrak{A}$ be a normed algebra over $\mathbb{K}$. Given a function $f : E \to \mathfrak{A}$ that is $C^n$-differentiable on a set $s \subseteq E$, then for any natural number $m$, the function $y \mapsto (f(y))^m$ is also $C^n$-differentiable on $s$.

ContDiffWithinAt.div_const theorem

{f : E → 𝕜'} {n} (hf : ContDiffWithinAt 𝕜 n f s x) (c : 𝕜') : ContDiffWithinAt 𝕜 n (fun x => f x / c) s x

Full source

theorem ContDiffWithinAt.div_const {f : E → 𝕜'} {n} (hf : ContDiffWithinAt 𝕜 n f s x) (c : 𝕜') :
    ContDiffWithinAt 𝕜 n (fun x => f x / c) s x := by
  simpa only [div_eq_mul_inv] using hf.mul contDiffWithinAt_const

$C^n$-Differentiability of Division by a Constant Within a Set at a Point

Informal description

Let $E$ be a normed space over a nontrivially normed field $\mathbb{K}$, $\mathbb{K}'$ be a normed algebra over $\mathbb{K}$, and $s \subseteq E$ be a subset. For a function $f : E \to \mathbb{K}'$ that is $C^n$-differentiable within $s$ at a point $x \in E$, and for any constant $c \in \mathbb{K}'$, the function $x \mapsto f(x) / c$ is also $C^n$-differentiable within $s$ at $x$.

ContDiffAt.div_const theorem

{f : E → 𝕜'} {n} (hf : ContDiffAt 𝕜 n f x) (c : 𝕜') : ContDiffAt 𝕜 n (fun x => f x / c) x

Full source

nonrec theorem ContDiffAt.div_const {f : E → 𝕜'} {n} (hf : ContDiffAt 𝕜 n f x) (c : 𝕜') :
    ContDiffAt 𝕜 n (fun x => f x / c) x :=
  hf.div_const c

$C^n$-Differentiability of Division by a Constant at a Point in Normed Algebras

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $E$ be a normed space over $\mathbb{K}$, and $\mathbb{K}'$ be a normed algebra over $\mathbb{K}$. For any function $f : E \to \mathbb{K}'$ that is $C^n$-differentiable at a point $x \in E$, and for any constant $c \in \mathbb{K}'$, the function $x \mapsto f(x) / c$ is also $C^n$-differentiable at $x$.

ContDiffOn.div_const theorem

{f : E → 𝕜'} {n} (hf : ContDiffOn 𝕜 n f s) (c : 𝕜') : ContDiffOn 𝕜 n (fun x => f x / c) s

Full source

theorem ContDiffOn.div_const {f : E → 𝕜'} {n} (hf : ContDiffOn 𝕜 n f s) (c : 𝕜') :
    ContDiffOn 𝕜 n (fun x => f x / c) s := fun x hx => (hf x hx).div_const c

$C^n$-Differentiability of Division by a Constant on a Set

Informal description

Let $E$ be a normed space over a nontrivially normed field $\mathbb{K}$, $\mathbb{K}'$ be a normed algebra over $\mathbb{K}$, and $s \subseteq E$ be a subset. If a function $f : E \to \mathbb{K}'$ is $C^n$-differentiable on $s$ and $c \in \mathbb{K}'$ is a constant, then the function $x \mapsto f(x) / c$ is also $C^n$-differentiable on $s$.

ContDiff.div_const theorem

{f : E → 𝕜'} {n} (hf : ContDiff 𝕜 n f) (c : 𝕜') : ContDiff 𝕜 n fun x => f x / c

Full source

theorem ContDiff.div_const {f : E → 𝕜'} {n} (hf : ContDiff 𝕜 n f) (c : 𝕜') :
    ContDiff 𝕜 n fun x => f x / c := by simpa only [div_eq_mul_inv] using hf.mul contDiff_const

$C^n$-Differentiability of Division by a Constant in Normed Algebras

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $E$ be a normed space over $\mathbb{K}$, and $\mathbb{K}'$ be a normed algebra over $\mathbb{K}$. For any function $f : E \to \mathbb{K}'$ that is $C^n$-differentiable (continuously differentiable of order $n$) over $\mathbb{K}$ and any constant $c \in \mathbb{K}'$, the function $x \mapsto f(x) / c$ is also $C^n$-differentiable over $\mathbb{K}$.

contDiff_smul theorem

: ContDiff 𝕜 n fun p : 𝕜 × F => p.1 • p.2

Full source

theorem contDiff_smul : ContDiff 𝕜 n fun p : 𝕜 × F => p.1 • p.2 :=
  isBoundedBilinearMap_smul.contDiff

Scalar multiplication is $C^n$-smooth

Informal description

Let $\mathbb{K}$ be a nontrivially normed field and $F$ be a normed space over $\mathbb{K}$. For any extended natural number $n \in \mathbb{N}_\infty$, the scalar multiplication operation $(λ, x) \mapsto λ \cdot x$ from $\mathbb{K} \times F$ to $F$ is $n$ times continuously differentiable (i.e., $C^n$).

ContDiffWithinAt.smul theorem

 {s : Set E} {f : E → 𝕜} {g : E → F} (hf : ContDiffWithinAt 𝕜 n f s x) (hg : ContDiffWithinAt 𝕜 n g s x) :
  ContDiffWithinAt 𝕜 n (fun x => f x • g x) s x

Full source

/-- The scalar multiplication of two `C^n` functions within a set at a point is `C^n` within this
set at this point. -/
theorem ContDiffWithinAt.smul {s : Set E} {f : E → 𝕜} {g : E → F} (hf : ContDiffWithinAt 𝕜 n f s x)
    (hg : ContDiffWithinAt 𝕜 n g s x) : ContDiffWithinAt 𝕜 n (fun x => f x • g x) s x :=
  contDiff_smul.contDiffWithinAt.comp x (hf.prodMk hg) subset_preimage_univ

Pointwise scalar product preserves $C^n$ differentiability within a set at a point

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $E$ and $F$ be normed spaces over $\mathbb{K}$, and $n \in \mathbb{N}_\infty$. Given a subset $s \subseteq E$ and a point $x \in E$, if $f : E \to \mathbb{K}$ and $g : E \to F$ are both $C^n$-differentiable within $s$ at $x$, then their pointwise scalar product $x \mapsto f(x) \cdot g(x)$ is also $C^n$-differentiable within $s$ at $x$.

ContDiffAt.smul theorem

 {f : E → 𝕜} {g : E → F} (hf : ContDiffAt 𝕜 n f x) (hg : ContDiffAt 𝕜 n g x) : ContDiffAt 𝕜 n (fun x => f x • g x) x

Full source

/-- The scalar multiplication of two `C^n` functions at a point is `C^n` at this point. -/
theorem ContDiffAt.smul {f : E → 𝕜} {g : E → F} (hf : ContDiffAt 𝕜 n f x)
    (hg : ContDiffAt 𝕜 n g x) : ContDiffAt 𝕜 n (fun x => f x • g x) x := by
  rw [← contDiffWithinAt_univ] at *; exact hf.smul hg

Pointwise scalar product preserves $C^n$ differentiability at a point

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $E$ and $F$ be normed spaces over $\mathbb{K}$, and $n \in \mathbb{N}_\infty$. Given a point $x \in E$, if $f : E \to \mathbb{K}$ and $g : E \to F$ are both $C^n$-differentiable at $x$, then their pointwise scalar product $x \mapsto f(x) \cdot g(x)$ is also $C^n$-differentiable at $x$.

ContDiff.smul theorem

{f : E → 𝕜} {g : E → F} (hf : ContDiff 𝕜 n f) (hg : ContDiff 𝕜 n g) : ContDiff 𝕜 n fun x => f x • g x

Full source

/-- The scalar multiplication of two `C^n` functions is `C^n`. -/
theorem ContDiff.smul {f : E → 𝕜} {g : E → F} (hf : ContDiff 𝕜 n f) (hg : ContDiff 𝕜 n g) :
    ContDiff 𝕜 n fun x => f x • g x :=
  contDiff_smul.comp (hf.prodMk hg)

Pointwise scalar product preserves $C^n$ differentiability

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $E$ and $F$ be normed spaces over $\mathbb{K}$, and $n \in \mathbb{N}_\infty$. If $f : E \to \mathbb{K}$ and $g : E \to F$ are both $C^n$ functions, then their pointwise scalar product $x \mapsto f(x) \cdot g(x)$ is also a $C^n$ function.

ContDiffOn.smul theorem

 {s : Set E} {f : E → 𝕜} {g : E → F} (hf : ContDiffOn 𝕜 n f s) (hg : ContDiffOn 𝕜 n g s) :
  ContDiffOn 𝕜 n (fun x => f x • g x) s

Full source

/-- The scalar multiplication of two `C^n` functions on a domain is `C^n`. -/
theorem ContDiffOn.smul {s : Set E} {f : E → 𝕜} {g : E → F} (hf : ContDiffOn 𝕜 n f s)
    (hg : ContDiffOn 𝕜 n g s) : ContDiffOn 𝕜 n (fun x => f x • g x) s := fun x hx =>
  (hf x hx).smul (hg x hx)

Pointwise scalar product preserves $C^n$ differentiability on a set

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $E$ and $F$ be normed spaces over $\mathbb{K}$, and $n \in \mathbb{N}_\infty$. Given a subset $s \subseteq E$, if $f : E \to \mathbb{K}$ and $g : E \to F$ are both $C^n$-differentiable on $s$, then their pointwise scalar product $x \mapsto f(x) \cdot g(x)$ is also $C^n$-differentiable on $s$.

contDiff_const_smul theorem

(c : R) : ContDiff 𝕜 n fun p : F => c • p

Full source

theorem contDiff_const_smul (c : R) : ContDiff 𝕜 n fun p : F => c • p :=
  (c • ContinuousLinearMap.id 𝕜 F).contDiff

Constant Scalar Multiplication Preserves $C^n$ Differentiability

Informal description

For any scalar $c$ in a normed space $R$ over a nontrivially normed field $\mathbb{K}$, the function $p \mapsto c \cdot p$ is $n$ times continuously differentiable ($C^n$) as a function from $F$ to itself, where $F$ is a normed space over $\mathbb{K}$.

ContDiffWithinAt.const_smul theorem

 {s : Set E} {f : E → F} {x : E} (c : R) (hf : ContDiffWithinAt 𝕜 n f s x) : ContDiffWithinAt 𝕜 n (fun y => c • f y) s x

Full source

/-- The scalar multiplication of a constant and a `C^n` function within a set at a point is `C^n`
within this set at this point. -/
theorem ContDiffWithinAt.const_smul {s : Set E} {f : E → F} {x : E} (c : R)
    (hf : ContDiffWithinAt 𝕜 n f s x) : ContDiffWithinAt 𝕜 n (fun y => c • f y) s x :=
  (contDiff_const_smul c).contDiffAt.comp_contDiffWithinAt x hf

Scalar multiplication preserves $C^n$ differentiability within a set at a point

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function that is $C^n$ within a set $s \subseteq E$ at a point $x \in E$. Then for any scalar $c \in R$, the function $y \mapsto c \cdot f(y)$ is also $C^n$ within $s$ at $x$.

ContDiffAt.const_smul theorem

{f : E → F} {x : E} (c : R) (hf : ContDiffAt 𝕜 n f x) : ContDiffAt 𝕜 n (fun y => c • f y) x

Full source

/-- The scalar multiplication of a constant and a `C^n` function at a point is `C^n` at this
point. -/
theorem ContDiffAt.const_smul {f : E → F} {x : E} (c : R) (hf : ContDiffAt 𝕜 n f x) :
    ContDiffAt 𝕜 n (fun y => c • f y) x := by
  rw [← contDiffWithinAt_univ] at *; exact hf.const_smul c

Scalar Multiplication Preserves $C^n$ Differentiability at a Point

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function that is $C^n$ at a point $x \in E$. Then for any scalar $c \in R$, the function $y \mapsto c \cdot f(y)$ is also $C^n$ at $x$.

ContDiff.const_smul theorem

{f : E → F} (c : R) (hf : ContDiff 𝕜 n f) : ContDiff 𝕜 n fun y => c • f y

Full source

/-- The scalar multiplication of a constant and a `C^n` function is `C^n`. -/
theorem ContDiff.const_smul {f : E → F} (c : R) (hf : ContDiff 𝕜 n f) :
    ContDiff 𝕜 n fun y => c • f y :=
  (contDiff_const_smul c).comp hf

Scalar multiplication preserves $C^n$ differentiability

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a $C^n$ function. Then for any scalar $c \in R$, the function $y \mapsto c \cdot f(y)$ is also $C^n$.

ContDiffOn.const_smul theorem

{s : Set E} {f : E → F} (c : R) (hf : ContDiffOn 𝕜 n f s) : ContDiffOn 𝕜 n (fun y => c • f y) s

Full source

/-- The scalar multiplication of a constant and a `C^n` on a domain is `C^n`. -/
theorem ContDiffOn.const_smul {s : Set E} {f : E → F} (c : R) (hf : ContDiffOn 𝕜 n f s) :
    ContDiffOn 𝕜 n (fun y => c • f y) s := fun x hx => (hf x hx).const_smul c

Scalar multiplication preserves $C^n$ differentiability on a set

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a $C^n$ function on a set $s \subseteq E$. Then for any scalar $c \in R$, the function $y \mapsto c \cdot f(y)$ is also $C^n$ on $s$.

iteratedFDerivWithin_const_smul_apply theorem

 (hf : ContDiffWithinAt 𝕜 i f s x) (hu : UniqueDiffOn 𝕜 s) (hx : x ∈ s) :
  iteratedFDerivWithin 𝕜 i (a • f) s x = a • iteratedFDerivWithin 𝕜 i f s x

Full source

theorem iteratedFDerivWithin_const_smul_apply (hf : ContDiffWithinAt 𝕜 i f s x)
    (hu : UniqueDiffOn 𝕜 s) (hx : x ∈ s) :
    iteratedFDerivWithin 𝕜 i (a • f) s x = a • iteratedFDerivWithin 𝕜 i f s x :=
  (a • (1 : F →L[𝕜] F)).iteratedFDerivWithin_comp_left hf hu hx le_rfl

Scalar Multiplication Commutes with Iterated Fréchet Derivative within a Set

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, $s \subseteq E$ a set with unique differentiability on $\mathbb{K}$, and $f : E \to F$ a function that is $C^i$ within $s$ at $x \in s$. Then for any scalar $a \in \mathbb{K}$, the $i$-th iterated Fréchet derivative within $s$ of the scaled function $a \cdot f$ at $x$ equals $a$ times the $i$-th iterated Fréchet derivative within $s$ of $f$ at $x$, i.e., $$ D^i_s(a \cdot f)(x) = a \cdot D^i_s f(x). $$

iteratedFDeriv_const_smul_apply' theorem

(hf : ContDiffAt 𝕜 i f x) : iteratedFDeriv 𝕜 i (fun x ↦ a • f x) x = a • iteratedFDeriv 𝕜 i f x

Full source

theorem iteratedFDeriv_const_smul_apply' (hf : ContDiffAt 𝕜 i f x) :
    iteratedFDeriv 𝕜 i (fun x ↦ a • f x) x = a • iteratedFDeriv 𝕜 i f x :=
  iteratedFDeriv_const_smul_apply hf

Scalar Multiplication Commutes with Iterated Fréchet Derivative at a Point

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function that is $C^i$ at a point $x \in E$. Then for any scalar $a \in \mathbb{K}$, the $i$-th iterated Fréchet derivative of the function $x \mapsto a \cdot f(x)$ at $x$ equals $a$ times the $i$-th iterated Fréchet derivative of $f$ at $x$, i.e., $$ D^i(a \cdot f)(x) = a \cdot D^i f(x). $$

ContDiffWithinAt.prodMap' theorem

 {s : Set E} {t : Set E'} {f : E → F} {g : E' → F'} {p : E × E'} (hf : ContDiffWithinAt 𝕜 n f s p.1)
  (hg : ContDiffWithinAt 𝕜 n g t p.2) : ContDiffWithinAt 𝕜 n (Prod.map f g) (s ×ˢ t) p

Full source

/-- The product map of two `C^n` functions within a set at a point is `C^n`
within the product set at the product point. -/
theorem ContDiffWithinAt.prodMap' {s : Set E} {t : Set E'} {f : E → F} {g : E' → F'} {p : E × E'}
    (hf : ContDiffWithinAt 𝕜 n f s p.1) (hg : ContDiffWithinAt 𝕜 n g t p.2) :
    ContDiffWithinAt 𝕜 n (Prod.map f g) (s ×ˢ t) p :=
  (hf.comp p contDiffWithinAt_fst (prod_subset_preimage_fst _ _)).prodMk
    (hg.comp p contDiffWithinAt_snd (prod_subset_preimage_snd _ _))

$C^n$ Differentiability of Product Map on Product Sets

Informal description

Let $E$, $E'$, $F$, $F'$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $s \subseteq E$, $t \subseteq E'$ be subsets. Given functions $f : E \to F$ and $g : E' \to F'$ that are $C^n$ within $s$ at $p.1$ and within $t$ at $p.2$ respectively, the product map $(f, g) : E \times E' \to F \times F'$ is $C^n$ within the product set $s \times t$ at the point $p = (p.1, p.2)$.

ContDiffWithinAt.prodMap theorem

 {s : Set E} {t : Set E'} {f : E → F} {g : E' → F'} {x : E} {y : E'} (hf : ContDiffWithinAt 𝕜 n f s x)
  (hg : ContDiffWithinAt 𝕜 n g t y) : ContDiffWithinAt 𝕜 n (Prod.map f g) (s ×ˢ t) (x, y)

Full source

theorem ContDiffWithinAt.prodMap {s : Set E} {t : Set E'} {f : E → F} {g : E' → F'} {x : E} {y : E'}
    (hf : ContDiffWithinAt 𝕜 n f s x) (hg : ContDiffWithinAt 𝕜 n g t y) :
    ContDiffWithinAt 𝕜 n (Prod.map f g) (s ×ˢ t) (x, y) :=
  ContDiffWithinAt.prodMap' hf hg

$C^n$ Differentiability of Product Map at a Point in Product Sets

Informal description

Let $E$, $E'$, $F$, $F'$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $s \subseteq E$, $t \subseteq E'$ be subsets. Given functions $f : E \to F$ and $g : E' \to F'$ that are $C^n$ within $s$ at $x$ and within $t$ at $y$ respectively, the product map $(f, g) : E \times E' \to F \times F'$ is $C^n$ within the product set $s \times t$ at the point $(x, y)$.

ContDiffOn.prodMap theorem

 {E' : Type*} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {F' : Type*} [NormedAddCommGroup F'] [NormedSpace 𝕜 F']
  {s : Set E} {t : Set E'} {f : E → F} {g : E' → F'} (hf : ContDiffOn 𝕜 n f s) (hg : ContDiffOn 𝕜 n g t) :
  ContDiffOn 𝕜 n (Prod.map f g) (s ×ˢ t)

Full source

/-- The product map of two `C^n` functions on a set is `C^n` on the product set. -/
theorem ContDiffOn.prodMap {E' : Type*} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {F' : Type*}
    [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] {s : Set E} {t : Set E'} {f : E → F} {g : E' → F'}
    (hf : ContDiffOn 𝕜 n f s) (hg : ContDiffOn 𝕜 n g t) : ContDiffOn 𝕜 n (Prod.map f g) (s ×ˢ t) :=
  (hf.comp contDiffOn_fst (prod_subset_preimage_fst _ _)).prodMk
    (hg.comp contDiffOn_snd (prod_subset_preimage_snd _ _))

$C^n$ Differentiability of Product Map on Product Sets

Informal description

Let $E$, $E'$, $F$, $F'$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $s \subseteq E$, $t \subseteq E'$ be subsets. If $f : E \to F$ is $C^n$ on $s$ and $g : E' \to F'$ is $C^n$ on $t$, then the product map $(f, g) : E \times E' \to F \times F'$ is $C^n$ on the product set $s \times t$.

ContDiffAt.prodMap theorem

 {f : E → F} {g : E' → F'} {x : E} {y : E'} (hf : ContDiffAt 𝕜 n f x) (hg : ContDiffAt 𝕜 n g y) :
  ContDiffAt 𝕜 n (Prod.map f g) (x, y)

Full source

/-- The product map of two `C^n` functions within a set at a point is `C^n`
within the product set at the product point. -/
theorem ContDiffAt.prodMap {f : E → F} {g : E' → F'} {x : E} {y : E'} (hf : ContDiffAt 𝕜 n f x)
    (hg : ContDiffAt 𝕜 n g y) : ContDiffAt 𝕜 n (Prod.map f g) (x, y) := by
  rw [ContDiffAt] at *
  simpa only [univ_prod_univ] using hf.prodMap hg

$C^n$ Differentiability of Product Map at a Point

Informal description

Let $E$, $E'$, $F$, $F'$ be normed spaces over a nontrivially normed field $\mathbb{K}$. Given functions $f : E \to F$ and $g : E' \to F'$ that are $C^n$ at points $x \in E$ and $y \in E'$ respectively, the product map $(f, g) : E \times E' \to F \times F'$ is $C^n$ at the point $(x, y)$.

ContDiffAt.prodMap' theorem

 {f : E → F} {g : E' → F'} {p : E × E'} (hf : ContDiffAt 𝕜 n f p.1) (hg : ContDiffAt 𝕜 n g p.2) :
  ContDiffAt 𝕜 n (Prod.map f g) p

Full source

/-- The product map of two `C^n` functions within a set at a point is `C^n`
within the product set at the product point. -/
theorem ContDiffAt.prodMap' {f : E → F} {g : E' → F'} {p : E × E'} (hf : ContDiffAt 𝕜 n f p.1)
    (hg : ContDiffAt 𝕜 n g p.2) : ContDiffAt 𝕜 n (Prod.map f g) p :=
  hf.prodMap hg

$C^n$ Differentiability of Product Map at a Point (General Form)

Informal description

Let $E$, $E'$, $F$, $F'$ be normed spaces over a nontrivially normed field $\mathbb{K}$. Given functions $f : E \to F$ and $g : E' \to F'$ that are $C^n$ at points $p_1 \in E$ and $p_2 \in E'$ respectively, where $p = (p_1, p_2) \in E \times E'$, then the product map $(f, g) : E \times E' \to F \times F'$ is $C^n$ at the point $p$.

ContDiff.prodMap theorem

{f : E → F} {g : E' → F'} (hf : ContDiff 𝕜 n f) (hg : ContDiff 𝕜 n g) : ContDiff 𝕜 n (Prod.map f g)

Full source

/-- The product map of two `C^n` functions is `C^n`. -/
theorem ContDiff.prodMap {f : E → F} {g : E' → F'} (hf : ContDiff 𝕜 n f) (hg : ContDiff 𝕜 n g) :
    ContDiff 𝕜 n (Prod.map f g) := by
  rw [contDiff_iff_contDiffAt] at *
  exact fun ⟨x, y⟩ => (hf x).prodMap (hg y)

$C^n$-differentiability of the product map of two $C^n$ functions

Informal description

Let $E$, $E'$, $F$, $F'$ be normed spaces over a nontrivially normed field $\mathbb{K}$. If $f : E \to F$ and $g : E' \to F'$ are $C^n$-differentiable functions, then the product map $(f, g) : E \times E' \to F \times F'$ is also $C^n$-differentiable.

contDiff_prodMk_left theorem

(f₀ : F) : ContDiff 𝕜 n fun e : E => (e, f₀)

Full source

theorem contDiff_prodMk_left (f₀ : F) : ContDiff 𝕜 n fun e : E => (e, f₀) :=
  contDiff_id.prodMk contDiff_const

$C^n$-differentiability of the left product map with a fixed element

Informal description

For any fixed element $f_0 \in F$, the function $e \mapsto (e, f_0)$ from $E$ to $E \times F$ is $C^n$-differentiable (i.e., continuously differentiable of order $n$) over the field $\mathbb{K}$.

contDiff_prodMk_right theorem

(e₀ : E) : ContDiff 𝕜 n fun f : F => (e₀, f)

Full source

theorem contDiff_prodMk_right (e₀ : E) : ContDiff 𝕜 n fun f : F => (e₀, f) :=
  contDiff_const.prodMk contDiff_id

Right projection is $C^n$-differentiable in product space

Informal description

For any fixed element $e_0 \in E$ in a normed space $E$ over a nontrivially normed field $\mathbb{K}$, the function mapping $f \in F$ to the pair $(e_0, f)$ is $C^n$-differentiable (continuously differentiable of order $n$) for any extended natural number $n \in \mathbb{N}_\infty$.

contDiffAt_ringInverse theorem

[HasSummableGeomSeries R] (x : Rˣ) : ContDiffAt 𝕜 n Ring.inverse (x : R)

Full source

/-- In a complete normed algebra, the operation of inversion is `C^n`, for all `n`, at each
invertible element, as it is analytic. -/
theorem contDiffAt_ringInverse [HasSummableGeomSeries R] (x : Rˣ) :
    ContDiffAt 𝕜 n Ring.inverse (x : R) := by
  have := AnalyticOnNhd.contDiffOn (analyticOnNhd_inverse (𝕜 := 𝕜) (A := R)) (n := n)
    Units.isOpen.uniqueDiffOn x x.isUnit
  exact this.contDiffAt (Units.isOpen.mem_nhds x.isUnit)

$C^n$-differentiability of inversion at units in normed algebras

Informal description

Let $R$ be a complete normed algebra over a nontrivially normed field $\mathbb{K}$ with summable geometric series. For any unit $x \in R^\times$, the ring inversion function $x \mapsto x^{-1}$ is $C^n$-differentiable at $x$ for any extended natural number $n \in \mathbb{N}_\infty$.

contDiffAt_inv theorem

{x : 𝕜'} (hx : x ≠ 0) {n} : ContDiffAt 𝕜 n Inv.inv x

Full source

theorem contDiffAt_inv {x : 𝕜'} (hx : x ≠ 0) {n} : ContDiffAt 𝕜 n Inv.inv x := by
  simpa only [Ring.inverse_eq_inv'] using contDiffAt_ringInverse 𝕜 (Units.mk0 x hx)

$C^n$-Differentiability of Inversion at Nonzero Points in Normed Fields

Informal description

For any nonzero element $x$ in a normed field $\mathbb{K}'$, the inversion function $x \mapsto x^{-1}$ is $C^n$-differentiable at $x$ for any extended natural number $n \in \mathbb{N}_\infty$.

contDiffOn_inv theorem

{n} : ContDiffOn 𝕜 n (Inv.inv : 𝕜' → 𝕜') {0}ᶜ

Full source

theorem contDiffOn_inv {n} : ContDiffOn 𝕜 n (Inv.inv : 𝕜' → 𝕜') {0}{0}ᶜ := fun _ hx =>
  (contDiffAt_inv 𝕜 hx).contDiffWithinAt

$C^n$-Differentiability of Inversion on Nonzero Elements of a Normed Field

Informal description

For any extended natural number $n \in \mathbb{N}_\infty$, the inversion function $x \mapsto x^{-1}$ is $C^n$-differentiable on the complement of $\{0\}$ in a normed field $\mathbb{K}'$.

ContDiffWithinAt.inv theorem

 {f : E → 𝕜'} {n} (hf : ContDiffWithinAt 𝕜 n f s x) (hx : f x ≠ 0) : ContDiffWithinAt 𝕜 n (fun x => (f x)⁻¹) s x

Full source

theorem ContDiffWithinAt.inv {f : E → 𝕜'} {n} (hf : ContDiffWithinAt 𝕜 n f s x) (hx : f x ≠ 0) :
    ContDiffWithinAt 𝕜 n (fun x => (f x)⁻¹) s x :=
  (contDiffAt_inv 𝕜 hx).comp_contDiffWithinAt x hf

$C^n$-Differentiability of Pointwise Inversion Within a Set

Informal description

Let $E$ be a normed space over a normed field $\mathbb{K}$, and let $\mathbb{K}'$ be a normed algebra over $\mathbb{K}$. Given a function $f : E \to \mathbb{K}'$ that is $C^n$-differentiable within a set $s \subseteq E$ at a point $x \in E$, and such that $f(x) \neq 0$, then the function $x \mapsto (f(x))^{-1}$ is also $C^n$-differentiable within $s$ at $x$.

ContDiffOn.inv theorem

{f : E → 𝕜'} (hf : ContDiffOn 𝕜 n f s) (h : ∀ x ∈ s, f x ≠ 0) : ContDiffOn 𝕜 n (fun x => (f x)⁻¹) s

Full source

theorem ContDiffOn.inv {f : E → 𝕜'} (hf : ContDiffOn 𝕜 n f s) (h : ∀ x ∈ s, f x ≠ 0) :
    ContDiffOn 𝕜 n (fun x => (f x)⁻¹) s := fun x hx => (hf.contDiffWithinAt hx).inv (h x hx)

$C^n$-Differentiability of Pointwise Inversion on a Set

Informal description

Let $E$ be a normed space over a normed field $\mathbb{K}$, and let $\mathbb{K}'$ be a normed algebra over $\mathbb{K}$. Given a function $f : E \to \mathbb{K}'$ that is $C^n$-differentiable on a set $s \subseteq E$, and such that $f(x) \neq 0$ for all $x \in s$, then the function $x \mapsto (f(x))^{-1}$ is also $C^n$-differentiable on $s$.

ContDiffAt.inv theorem

{f : E → 𝕜'} (hf : ContDiffAt 𝕜 n f x) (hx : f x ≠ 0) : ContDiffAt 𝕜 n (fun x => (f x)⁻¹) x

Full source

nonrec theorem ContDiffAt.inv {f : E → 𝕜'} (hf : ContDiffAt 𝕜 n f x) (hx : f x ≠ 0) :
    ContDiffAt 𝕜 n (fun x => (f x)⁻¹) x :=
  hf.inv hx

$C^n$-Differentiability of Pointwise Inversion at a Point

Informal description

Let $E$ be a normed space over a normed field $\mathbb{K}$, and let $\mathbb{K}'$ be a normed algebra over $\mathbb{K}$. Given a function $f : E \to \mathbb{K}'$ that is $C^n$-differentiable at a point $x \in E$, and such that $f(x) \neq 0$, then the function $x \mapsto (f(x))^{-1}$ is also $C^n$-differentiable at $x$.

ContDiff.inv theorem

{f : E → 𝕜'} (hf : ContDiff 𝕜 n f) (h : ∀ x, f x ≠ 0) : ContDiff 𝕜 n fun x => (f x)⁻¹

Full source

theorem ContDiff.inv {f : E → 𝕜'} (hf : ContDiff 𝕜 n f) (h : ∀ x, f x ≠ 0) :
    ContDiff 𝕜 n fun x => (f x)⁻¹ := by
  rw [contDiff_iff_contDiffAt]; exact fun x => hf.contDiffAt.inv (h x)

$C^n$-Differentiability of Pointwise Inversion

Informal description

Let $E$ be a normed space over a nontrivially normed field $\mathbb{K}$, and let $\mathbb{K}'$ be a normed algebra over $\mathbb{K}$. If a function $f : E \to \mathbb{K}'$ is $C^n$-differentiable and satisfies $f(x) \neq 0$ for all $x \in E$, then the function $x \mapsto (f(x))^{-1}$ is also $C^n$-differentiable.

ContDiffWithinAt.div theorem

 {f g : E → 𝕜} {n} (hf : ContDiffWithinAt 𝕜 n f s x) (hg : ContDiffWithinAt 𝕜 n g s x) (hx : g x ≠ 0) :
  ContDiffWithinAt 𝕜 n (fun x => f x / g x) s x

Full source

theorem ContDiffWithinAt.div {f g : E → 𝕜} {n} (hf : ContDiffWithinAt 𝕜 n f s x)
    (hg : ContDiffWithinAt 𝕜 n g s x) (hx : g x ≠ 0) :
    ContDiffWithinAt 𝕜 n (fun x => f x / g x) s x := by
  simpa only [div_eq_mul_inv] using hf.mul (hg.inv hx)

$C^n$-Differentiability of Pointwise Division Within a Set at a Point

Informal description

Let $E$ be a normed space over a nontrivially normed field $\mathbb{K}$, and let $s \subseteq E$ be a subset. For two functions $f, g : E \to \mathbb{K}$ that are $C^n$-differentiable within $s$ at a point $x \in E$, if $g(x) \neq 0$, then the function $x \mapsto \frac{f(x)}{g(x)}$ is also $C^n$-differentiable within $s$ at $x$.

ContDiffOn.div theorem

 {f g : E → 𝕜} {n} (hf : ContDiffOn 𝕜 n f s) (hg : ContDiffOn 𝕜 n g s) (h₀ : ∀ x ∈ s, g x ≠ 0) :
  ContDiffOn 𝕜 n (f / g) s

Full source

theorem ContDiffOn.div {f g : E → 𝕜} {n} (hf : ContDiffOn 𝕜 n f s)
    (hg : ContDiffOn 𝕜 n g s) (h₀ : ∀ x ∈ s, g x ≠ 0) : ContDiffOn 𝕜 n (f / g) s := fun x hx =>
  (hf x hx).div (hg x hx) (h₀ x hx)

$C^n$-Differentiability of Pointwise Division on a Set

Informal description

Let $E$ be a normed space over a nontrivially normed field $\mathbb{K}$, and let $s \subseteq E$ be a subset. For two functions $f, g : E \to \mathbb{K}$ that are $C^n$-differentiable on $s$, if $g(x) \neq 0$ for all $x \in s$, then the pointwise division function $\frac{f}{g} : x \mapsto \frac{f(x)}{g(x)}$ is also $C^n$-differentiable on $s$.

ContDiffAt.div theorem

 {f g : E → 𝕜} {n} (hf : ContDiffAt 𝕜 n f x) (hg : ContDiffAt 𝕜 n g x) (hx : g x ≠ 0) :
  ContDiffAt 𝕜 n (fun x => f x / g x) x

Full source

nonrec theorem ContDiffAt.div {f g : E → 𝕜} {n} (hf : ContDiffAt 𝕜 n f x)
    (hg : ContDiffAt 𝕜 n g x) (hx : g x ≠ 0) : ContDiffAt 𝕜 n (fun x => f x / g x) x :=
  hf.div hg hx

$C^n$-Differentiability of Pointwise Division at a Point

Informal description

Let $E$ be a normed space over a nontrivially normed field $\mathbb{K}$. For two functions $f, g : E \to \mathbb{K}$ that are $C^n$-differentiable at a point $x \in E$, if $g(x) \neq 0$, then the function $x \mapsto \frac{f(x)}{g(x)}$ is also $C^n$-differentiable at $x$.

ContDiff.div theorem

 {f g : E → 𝕜} {n} (hf : ContDiff 𝕜 n f) (hg : ContDiff 𝕜 n g) (h0 : ∀ x, g x ≠ 0) : ContDiff 𝕜 n fun x => f x / g x

Full source

theorem ContDiff.div {f g : E → 𝕜} {n} (hf : ContDiff 𝕜 n f) (hg : ContDiff 𝕜 n g)
    (h0 : ∀ x, g x ≠ 0) : ContDiff 𝕜 n fun x => f x / g x := by
  simp only [contDiff_iff_contDiffAt] at *
  exact fun x => (hf x).div (hg x) (h0 x)

$C^n$-Differentiability of Pointwise Division

Informal description

Let $E$ be a normed space over a nontrivially normed field $\mathbb{K}$. For two $C^n$-differentiable functions $f, g : E \to \mathbb{K}$, if $g(x) \neq 0$ for all $x \in E$, then the pointwise division function $x \mapsto \frac{f(x)}{g(x)}$ is also $C^n$-differentiable.

contDiffAt_map_inverse theorem

[CompleteSpace E] (e : E ≃L[𝕜] F) : ContDiffAt 𝕜 n inverse (e : E →L[𝕜] F)

Full source

/-- At a continuous linear equivalence `e : E ≃L[𝕜] F` between Banach spaces, the operation of
inversion is `C^n`, for all `n`. -/
theorem contDiffAt_map_inverse [CompleteSpace E] (e : E ≃L[𝕜] F) :
    ContDiffAt 𝕜 n inverse (e : E →L[𝕜] F) := by
  nontriviality E
  -- first, we use the lemma `inverse_eq_ringInverse` to rewrite in terms of `Ring.inverse` in the
  -- ring `E →L[𝕜] E`
  let O₁ : (E →L[𝕜] E) → F →L[𝕜] E := fun f => f.comp (e.symm : F →L[𝕜] E)
  let O₂ : (E →L[𝕜] F) → E →L[𝕜] E := fun f => (e.symm : F →L[𝕜] E).comp f
  have : ContinuousLinearMap.inverse = O₁ ∘ Ring.inverse ∘ O₂ := funext (inverse_eq_ringInverse e)
  rw [this]
  -- `O₁` and `O₂` are `ContDiff`,
  -- so we reduce to proving that `Ring.inverse` is `ContDiff`
  have h₁ : ContDiff 𝕜 n O₁ := contDiff_id.clm_comp contDiff_const
  have h₂ : ContDiff 𝕜 n O₂ := contDiff_const.clm_comp contDiff_id
  refine h₁.contDiffAt.comp _ (ContDiffAt.comp _ ?_ h₂.contDiffAt)
  convert contDiffAt_ringInverse 𝕜 (1 : (E →L[𝕜] E)ˣ)
  simp [O₂, one_def]

$C^n$-Differentiability of Inversion for Continuous Linear Equivalences Between Banach Spaces

Informal description

Let $E$ and $F$ be Banach spaces over a nontrivially normed field $\mathbb{K}$, with $E$ complete. For any continuous linear equivalence $e : E \simeq_{\mathbb{K}} F$, the operation of inversion (mapping $e$ to its inverse $e^{-1}$) is $C^n$-differentiable at $e$ for any extended natural number $n \in \mathbb{N}_\infty$.

ContinuousLinearMap.IsInvertible.contDiffAt_map_inverse theorem

[CompleteSpace E] {e : E →L[𝕜] F} (he : e.IsInvertible) : ContDiffAt 𝕜 n inverse e

Full source

/-- At an invertible map `e : M →L[R] M₂` between Banach spaces, the operation of
inversion is `C^n`, for all `n`. -/
theorem ContinuousLinearMap.IsInvertible.contDiffAt_map_inverse [CompleteSpace E] {e : E →L[𝕜] F}
    (he : e.IsInvertible) : ContDiffAt 𝕜 n inverse e := by
  rcases he with ⟨M, rfl⟩
  exact _root_.contDiffAt_map_inverse M

$C^n$-Differentiability of Inversion for Invertible Continuous Linear Maps Between Banach Spaces

Informal description

Let $E$ and $F$ be Banach spaces over a nontrivially normed field $\mathbb{K}$, with $E$ complete. For any invertible continuous linear map $e : E \to_{\mathbb{K}} F$, the operation of inversion (mapping $e$ to its inverse $e^{-1}$) is $C^n$-differentiable at $e$ for any extended natural number $n \in \mathbb{N}_\infty$.

PartialHomeomorph.contDiffAt_symm theorem

 [CompleteSpace E] (f : PartialHomeomorph E F) {f₀' : E ≃L[𝕜] F} {a : F} (ha : a ∈ f.target)
  (hf₀' : HasFDerivAt f (f₀' : E →L[𝕜] F) (f.symm a)) (hf : ContDiffAt 𝕜 n f (f.symm a)) : ContDiffAt 𝕜 n f.symm a

Full source

/-- If `f` is a local homeomorphism and the point `a` is in its target,
and if `f` is `n` times continuously differentiable at `f.symm a`,
and if the derivative at `f.symm a` is a continuous linear equivalence,
then `f.symm` is `n` times continuously differentiable at the point `a`.

This is one of the easy parts of the inverse function theorem: it assumes that we already have
an inverse function. -/
theorem PartialHomeomorph.contDiffAt_symm [CompleteSpace E] (f : PartialHomeomorph E F)
    {f₀' : E ≃L[𝕜] F} {a : F} (ha : a ∈ f.target)
    (hf₀' : HasFDerivAt f (f₀' : E →L[𝕜] F) (f.symm a)) (hf : ContDiffAt 𝕜 n f (f.symm a)) :
    ContDiffAt 𝕜 n f.symm a := by
  match n with
  | ω =>
    apply AnalyticAt.contDiffAt
    exact f.analyticAt_symm ha hf.analyticAt hf₀'.fderiv
  | (n : ℕ∞) =>
    -- We prove this by induction on `n`
    induction' n using ENat.nat_induction with n IH Itop
    · apply contDiffAt_zero.2
      exact ⟨f.target, IsOpen.mem_nhds f.open_target ha, f.continuousOn_invFun⟩
    · obtain ⟨f', ⟨u, hu, hff'⟩, hf'⟩ := contDiffAt_succ_iff_hasFDerivAt.mp hf
      apply contDiffAt_succ_iff_hasFDerivAt.2
      -- For showing `n.succ` times continuous differentiability (the main inductive step), it
      -- suffices to produce the derivative and show that it is `n` times continuously
      -- differentiable
      have eq_f₀' : f' (f.symm a) = f₀' := (hff' (f.symm a) (mem_of_mem_nhds hu)).unique hf₀'
      -- This follows by a bootstrapping formula expressing the derivative as a
      -- function of `f` itself
      refine ⟨inverse ∘ f' ∘ f.symm, ?_, ?_⟩
      · -- We first check that the derivative of `f` is that formula
        have h_nhds : { y : E | ∃ e : E ≃L[𝕜] F, ↑e = f' y }{ y : E | ∃ e : E ≃L[𝕜] F, ↑e = f' y } ∈ 𝓝 (f.symm a) := by
          have hf₀' := f₀'.nhds
          rw [← eq_f₀'] at hf₀'
          exact hf'.continuousAt.preimage_mem_nhds hf₀'
        obtain ⟨t, htu, ht, htf⟩ := mem_nhds_iff.mp (Filter.inter_mem hu h_nhds)
        use f.target ∩ f.symm ⁻¹' t
        refine ⟨IsOpen.mem_nhds ?_ ?_, ?_⟩
        · exact f.isOpen_inter_preimage_symm ht
        · exact mem_inter ha (mem_preimage.mpr htf)
        intro x hx
        obtain ⟨hxu, e, he⟩ := htu hx.2
        have h_deriv : HasFDerivAt f (e : E →L[𝕜] F) (f.symm x) := by
          rw [he]
          exact hff' (f.symm x) hxu
        convert f.hasFDerivAt_symm hx.1 h_deriv
        simp [← he]
      · -- Then we check that the formula, being a composition of `ContDiff` pieces, is
        -- itself `ContDiff`
        have h_deriv₁ : ContDiffAt 𝕜 n inverse (f' (f.symm a)) := by
          rw [eq_f₀']
          exact contDiffAt_map_inverse _
        have h_deriv₂ : ContDiffAt 𝕜 n f.symm a := by
          refine IH (hf.of_le ?_)
          norm_cast
          exact Nat.le_succ n
        exact (h_deriv₁.comp _ hf').comp _ h_deriv₂
    · refine contDiffAt_infty.mpr ?_
      intro n
      exact Itop n (contDiffAt_infty.mp hf n)

$C^n$ Differentiability of Inverse Function at a Point for Partial Homeomorphisms Between Banach Spaces

Informal description

Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, with $E$ complete. Given a partial homeomorphism $f : E \to F$, a point $a \in f.\text{target}$, and a continuous linear equivalence $f₀' : E \simeq_{\mathbb{K}} F$ such that: 1. $f$ has Fréchet derivative $f₀'$ at $f^{-1}(a)$, 2. $f$ is $C^n$ at $f^{-1}(a)$, then the inverse function $f^{-1}$ is $C^n$ at $a$.

Homeomorph.contDiff_symm theorem

 [CompleteSpace E] (f : E ≃ₜ F) {f₀' : E → E ≃L[𝕜] F} (hf₀' : ∀ a, HasFDerivAt f (f₀' a : E →L[𝕜] F) a)
  (hf : ContDiff 𝕜 n (f : E → F)) : ContDiff 𝕜 n (f.symm : F → E)

Full source

/-- If `f` is an `n` times continuously differentiable homeomorphism,
and if the derivative of `f` at each point is a continuous linear equivalence,
then `f.symm` is `n` times continuously differentiable.

This is one of the easy parts of the inverse function theorem: it assumes that we already have
an inverse function. -/
theorem Homeomorph.contDiff_symm [CompleteSpace E] (f : E ≃ₜ F) {f₀' : E → E ≃L[𝕜] F}
    (hf₀' : ∀ a, HasFDerivAt f (f₀' a : E →L[𝕜] F) a) (hf : ContDiff 𝕜 n (f : E → F)) :
    ContDiff 𝕜 n (f.symm : F → E) :=
  contDiff_iff_contDiffAt.2 fun x =>
    f.toPartialHomeomorph.contDiffAt_symm (mem_univ x) (hf₀' _) hf.contDiffAt

$C^n$ Differentiability of the Inverse of a Differentiable Homeomorphism Between Banach Spaces

Informal description

Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, with $E$ complete. Let $f : E \to F$ be a homeomorphism that is $n$ times continuously differentiable ($C^n$), and suppose that at every point $a \in E$, the Fréchet derivative $f₀'(a)$ of $f$ at $a$ is a continuous linear equivalence. Then the inverse function $f^{-1} : F \to E$ is also $n$ times continuously differentiable.

PartialHomeomorph.contDiffAt_symm_deriv theorem

 [CompleteSpace 𝕜] (f : PartialHomeomorph 𝕜 𝕜) {f₀' a : 𝕜} (h₀ : f₀' ≠ 0) (ha : a ∈ f.target)
  (hf₀' : HasDerivAt f f₀' (f.symm a)) (hf : ContDiffAt 𝕜 n f (f.symm a)) : ContDiffAt 𝕜 n f.symm a

Full source

/-- Let `f` be a local homeomorphism of a nontrivially normed field, let `a` be a point in its
target. if `f` is `n` times continuously differentiable at `f.symm a`, and if the derivative at
`f.symm a` is nonzero, then `f.symm` is `n` times continuously differentiable at the point `a`.

This is one of the easy parts of the inverse function theorem: it assumes that we already have
an inverse function. -/
theorem PartialHomeomorph.contDiffAt_symm_deriv [CompleteSpace 𝕜] (f : PartialHomeomorph 𝕜 𝕜)
    {f₀' a : 𝕜} (h₀ : f₀' ≠ 0) (ha : a ∈ f.target) (hf₀' : HasDerivAt f f₀' (f.symm a))
    (hf : ContDiffAt 𝕜 n f (f.symm a)) : ContDiffAt 𝕜 n f.symm a :=
  f.contDiffAt_symm ha (hf₀'.hasFDerivAt_equiv h₀) hf

$C^n$ Differentiability of Inverse Function at a Point with Nonzero Derivative

Informal description

Let $\mathbb{K}$ be a complete nontrivially normed field, and let $f$ be a local homeomorphism of $\mathbb{K}$. For a point $a$ in the target of $f$, suppose that: 1. $f$ is differentiable at $f^{-1}(a)$ with derivative $f₀' \neq 0$, 2. $f$ is $C^n$ at $f^{-1}(a)$. Then the inverse function $f^{-1}$ is $C^n$ at $a$.

Homeomorph.contDiff_symm_deriv theorem

 [CompleteSpace 𝕜] (f : 𝕜 ≃ₜ 𝕜) {f' : 𝕜 → 𝕜} (h₀ : ∀ x, f' x ≠ 0) (hf' : ∀ x, HasDerivAt f (f' x) x)
  (hf : ContDiff 𝕜 n (f : 𝕜 → 𝕜)) : ContDiff 𝕜 n (f.symm : 𝕜 → 𝕜)

Full source

/-- Let `f` be an `n` times continuously differentiable homeomorphism of a nontrivially normed
field.  Suppose that the derivative of `f` is never equal to zero. Then `f.symm` is `n` times
continuously differentiable.

This is one of the easy parts of the inverse function theorem: it assumes that we already have
an inverse function. -/
theorem Homeomorph.contDiff_symm_deriv [CompleteSpace 𝕜] (f : 𝕜 ≃ₜ 𝕜) {f' : 𝕜 → 𝕜}
    (h₀ : ∀ x, f' x ≠ 0) (hf' : ∀ x, HasDerivAt f (f' x) x) (hf : ContDiff 𝕜 n (f : 𝕜 → 𝕜)) :
    ContDiff 𝕜 n (f.symm : 𝕜 → 𝕜) :=
  contDiff_iff_contDiffAt.2 fun x =>
    f.toPartialHomeomorph.contDiffAt_symm_deriv (h₀ _) (mem_univ x) (hf' _) hf.contDiffAt

$C^n$ differentiability of inverse homeomorphism with nonzero derivative

Informal description

Let $\mathbb{K}$ be a complete nontrivially normed field and $f : \mathbb{K} \to \mathbb{K}$ be a homeomorphism. Suppose that: 1. $f$ has a derivative $f'(x)$ at every point $x \in \mathbb{K}$, with $f'(x) \neq 0$ for all $x$, 2. $f$ is $n$ times continuously differentiable ($C^n$) on $\mathbb{K}$. Then the inverse function $f^{-1}$ is also $n$ times continuously differentiable on $\mathbb{K}$.

PartialHomeomorph.restrContDiff definition

(f : PartialHomeomorph E F) (n : WithTop ℕ∞) (hn : n ≠ ∞) : PartialHomeomorph E F

Full source

/-- Restrict a partial homeomorphism to the subsets of the source and target
that consist of points `x ∈ f.source`, `y = f x ∈ f.target`
such that `f` is `C^n` at `x` and `f.symm` is `C^n` at `y`.

Note that `n` is a natural number or `ω`, but not `∞`,
because the set of points of `C^∞`-smoothness of `f` is not guaranteed to be open. -/
@[simps! apply symm_apply source target]
def restrContDiff (f : PartialHomeomorph E F) (n : WithTop ℕ∞) (hn : n ≠ ∞) :
    PartialHomeomorph E F :=
  haveI H : f.IsImage {x | ContDiffAt 𝕜 n f x ∧ ContDiffAt 𝕜 n f.symm (f x)}
      {y | ContDiffAt 𝕜 n f.symm y ∧ ContDiffAt 𝕜 n f (f.symm y)} := fun x hx ↦ by
    simp [hx, and_comm]
  H.restr <| isOpen_iff_mem_nhds.2 fun _ ⟨hxs, hxf, hxf'⟩ ↦
    inter_mem (f.open_source.mem_nhds hxs) <| (hxf.eventually hn).and <|
    f.continuousAt hxs (hxf'.eventually hn)

Restriction of a partial homeomorphism to $ C^n $-smooth points

Informal description

Given a partial homeomorphism $ f $ between normed spaces $ E $ and $ F $ over a nontrivially normed field $ \mathbb{K} $, and an extended natural number $ n \neq \infty $, the restriction $ f \restriction_{C^n} $ is a partial homeomorphism defined on the subsets: - Source: $ \{x \in f.\text{source} \mid f \text{ is } C^n \text{ at } x \text{ and } f^{-1} \text{ is } C^n \text{ at } f(x)\} $ - Target: $ \{y \in f.\text{target} \mid f^{-1} \text{ is } C^n \text{ at } y \text{ and } f \text{ is } C^n \text{ at } f^{-1}(y)\} $ This restriction is well-defined and maintains the partial homeomorphism structure, with the forward and inverse maps being $ C^n $ on their respective domains.

PartialHomeomorph.contDiffOn_restrContDiff_source theorem

 (f : PartialHomeomorph E F) {n : WithTop ℕ∞} (hn : n ≠ ∞) : ContDiffOn 𝕜 n f (f.restrContDiff 𝕜 n hn).source

Full source

lemma contDiffOn_restrContDiff_source (f : PartialHomeomorph E F) {n : WithTop ℕ∞} (hn : n ≠ ∞) :
    ContDiffOn 𝕜 n f (f.restrContDiff 𝕜 n hn).source := fun _x hx ↦ hx.2.1.contDiffWithinAt

$C^n$-Differentiability of Restricted Partial Homeomorphism on Source Set

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $f$ be a partial homeomorphism between $E$ and $F$. For any extended natural number $n \neq \infty$, the restriction of $f$ to the set of points where both $f$ and its inverse are $C^n$-differentiable is itself $C^n$-differentiable on its source set.

PartialHomeomorph.contDiffOn_restrContDiff_target theorem

 (f : PartialHomeomorph E F) {n : WithTop ℕ∞} (hn : n ≠ ∞) : ContDiffOn 𝕜 n f.symm (f.restrContDiff 𝕜 n hn).target

Full source

lemma contDiffOn_restrContDiff_target (f : PartialHomeomorph E F) {n : WithTop ℕ∞} (hn : n ≠ ∞) :
    ContDiffOn 𝕜 n f.symm (f.restrContDiff 𝕜 n hn).target := fun _x hx ↦ hx.2.1.contDiffWithinAt

$C^n$-Differentiability of Inverse on Restricted Target Set

Informal description

Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $f$ be a partial homeomorphism between $E$ and $F$. For any extended natural number $n \neq \infty$, the inverse function $f^{-1}$ is $C^n$-differentiable on the target set of the restricted partial homeomorphism $f \restriction_{C^n}$.

HasFTaylorSeriesUpToOn.restrictScalars theorem

 {n : WithTop ℕ∞} (h : HasFTaylorSeriesUpToOn n f p' s) :
  HasFTaylorSeriesUpToOn n f (fun x => (p' x).restrictScalars 𝕜) s

Full source

theorem HasFTaylorSeriesUpToOn.restrictScalars {n : WithTop ℕ∞}
    (h : HasFTaylorSeriesUpToOn n f p' s) :
    HasFTaylorSeriesUpToOn n f (fun x => (p' x).restrictScalars 𝕜) s where
  zero_eq x hx := h.zero_eq x hx
  fderivWithin m hm x hx :=
    ((ContinuousMultilinearMap.restrictScalarsLinear 𝕜).hasFDerivAt.comp_hasFDerivWithinAt x <|
        (h.fderivWithin m hm x hx).restrictScalars 𝕜 :)
  cont m hm := ContinuousMultilinearMap.continuous_restrictScalars.comp_continuousOn (h.cont m hm)

Restriction of Scalars Preserves Formal Taylor Series

Informal description

Let $E$ and $F$ be normed spaces over normed fields $\mathbb{K}$ and $\mathbb{K}'$ respectively, with $\mathbb{K}$ a subfield of $\mathbb{K}'$ via a normed algebra structure. Given a function $f : E \to F$, a set $s \subseteq E$, and an extended natural number $n \in \mathbb{N}_\infty$, if $f$ has a formal Taylor series $p'$ up to order $n$ on $s$ as a $\mathbb{K}'$-valued function, then $f$ also has a formal Taylor series up to order $n$ on $s$ when considered as a $\mathbb{K}$-valued function, obtained by restricting the scalars of $p'$ from $\mathbb{K}'$ to $\mathbb{K}$.

ContDiffWithinAt.restrict_scalars theorem

(h : ContDiffWithinAt 𝕜' n f s x) : ContDiffWithinAt 𝕜 n f s x

Full source

theorem ContDiffWithinAt.restrict_scalars (h : ContDiffWithinAt 𝕜' n f s x) :
    ContDiffWithinAt 𝕜 n f s x := by
  match n with
  | ω =>
    obtain ⟨u, u_mem, p', hp', Hp'⟩ := h
    refine ⟨u, u_mem, _, hp'.restrictScalars _, fun i ↦ ?_⟩
    change AnalyticOn 𝕜 (fun x ↦ ContinuousMultilinearMap.restrictScalarsLinear 𝕜 (p' x i)) u
    apply AnalyticOnNhd.comp_analyticOn _ (Hp' i).restrictScalars (Set.mapsTo_univ _ _)
    exact ContinuousLinearMap.analyticOnNhd _ _
  | (n : ℕ∞) =>
    intro m hm
    rcases h m hm with ⟨u, u_mem, p', hp'⟩
    exact ⟨u, u_mem, _, hp'.restrictScalars _⟩

Restriction of Scalars Preserves $C^n$ Differentiability Within a Set at a Point

Informal description

Let $\mathbb{K}$ and $\mathbb{K}'$ be normed fields with $\mathbb{K}$ a subfield of $\mathbb{K}'$, and let $E$ and $F$ be normed spaces over $\mathbb{K}'$. If a function $f : E \to F$ is $C^n$ within a set $s \subseteq E$ at a point $x \in E$ with respect to $\mathbb{K}'$, then $f$ is also $C^n$ within $s$ at $x$ with respect to $\mathbb{K}$.

ContDiffOn.restrict_scalars theorem

(h : ContDiffOn 𝕜' n f s) : ContDiffOn 𝕜 n f s

Full source

theorem ContDiffOn.restrict_scalars (h : ContDiffOn 𝕜' n f s) : ContDiffOn 𝕜 n f s := fun x hx =>
  (h x hx).restrict_scalars _

Restriction of Scalars Preserves $C^n$ Differentiability on a Set

Informal description

Let $\mathbb{K}$ and $\mathbb{K}'$ be normed fields with $\mathbb{K}$ a subfield of $\mathbb{K}'$, and let $E$ and $F$ be normed spaces over $\mathbb{K}'$. If a function $f : E \to F$ is $C^n$ on a set $s \subseteq E$ with respect to $\mathbb{K}'$, then $f$ is also $C^n$ on $s$ with respect to $\mathbb{K}$.

ContDiffAt.restrict_scalars theorem

(h : ContDiffAt 𝕜' n f x) : ContDiffAt 𝕜 n f x

Full source

theorem ContDiffAt.restrict_scalars (h : ContDiffAt 𝕜' n f x) : ContDiffAt 𝕜 n f x :=
  contDiffWithinAt_univ.1 <| h.contDiffWithinAt.restrict_scalars _

Restriction of Scalars Preserves $C^n$ Differentiability at a Point

Informal description

Let $\mathbb{K}$ and $\mathbb{K}'$ be normed fields with $\mathbb{K}$ a subfield of $\mathbb{K}'$, and let $E$ and $F$ be normed spaces over $\mathbb{K}'$. If a function $f : E \to F$ is $C^n$ at a point $x \in E$ with respect to $\mathbb{K}'$, then $f$ is also $C^n$ at $x$ with respect to $\mathbb{K}$.

ContDiff.restrict_scalars theorem

(h : ContDiff 𝕜' n f) : ContDiff 𝕜 n f

Full source

theorem ContDiff.restrict_scalars (h : ContDiff 𝕜' n f) : ContDiff 𝕜 n f :=
  contDiff_iff_contDiffAt.2 fun _ => h.contDiffAt.restrict_scalars _

Restriction of Scalars Preserves $C^n$ Differentiability

Informal description

Let $\mathbb{K}$ and $\mathbb{K}'$ be normed fields with $\mathbb{K}$ a subfield of $\mathbb{K}'$, and let $E$ and $F$ be normed spaces over $\mathbb{K}'$. If a function $f : E \to F$ is $C^n$ (continuously differentiable of order $n$) with respect to $\mathbb{K}'$, then $f$ is also $C^n$ with respect to $\mathbb{K}$.

Mathlib.Analysis.Calculus.ContDiff.Operations

Notations

Tags