Higher differentiability of usual operations

We prove that the usual operations (addition, multiplication, difference, and so on) preserve C^n functions.

Notation

We use the notation E [×n]→L[𝕜] F for the space of continuous multilinear maps on E^n with values in F. This is the space in which the n-th derivative of a function from E to F lives.

In this file, we denote WithTop ℕ∞ with ℕ∞ω, (⊤ : ℕ∞) : ℕ∞ω with ∞ and ⊤ : ℕ∞ω with ω.

Tags

derivative, differentiability, higher derivative, C^n, multilinear, Taylor series, formal series

Smoothness of functions f : E → Π i, F' i

theorem hasFTaylorSeriesUpToOn_pi {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {s : Set E} {ι : Type u_3} [Fintype ι] {F' : ι → Type u_5} [(i : ι) → NormedAddCommGroup (F' i)] [(i : ι) → NormedSpace 𝕜 (F' i)] {φ : (i : ι) → E → F' i} {p' : (i : ι) → E → FormalMultilinearSeries 𝕜 E (F' i)} {n : WithTop ℕ∞} : HasFTaylorSeriesUpToOn n (fun (x : E) (i : ι) => φ i x) (fun (x : E) (m : ℕ) => ContinuousMultilinearMap.pi fun (i : ι) => p' i x m) s ↔ ∀ (i : ι), HasFTaylorSeriesUpToOn n (φ i) (p' i) s

@[simp]

theorem hasFTaylorSeriesUpToOn_pi' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {s : Set E} {ι : Type u_3} [Fintype ι] {F' : ι → Type u_5} [(i : ι) → NormedAddCommGroup (F' i)] [(i : ι) → NormedSpace 𝕜 (F' i)] {Φ : E → (i : ι) → F' i} {P' : E → FormalMultilinearSeries 𝕜 E ((i : ι) → F' i)} {n : WithTop ℕ∞} : HasFTaylorSeriesUpToOn n Φ P' s ↔ ∀ (i : ι), HasFTaylorSeriesUpToOn n (fun (x : E) => Φ x i) (fun (x : E) (m : ℕ) => (ContinuousLinearMap.proj i).compContinuousMultilinearMap (P' x m)) s

theorem contDiffWithinAt_pi {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {s : Set E} {x : E} {n : WithTop ℕ∞} {ι : Type u_3} [Fintype ι] {F' : ι → Type u_5} [(i : ι) → NormedAddCommGroup (F' i)] [(i : ι) → NormedSpace 𝕜 (F' i)] {Φ : E → (i : ι) → F' i} : ContDiffWithinAt 𝕜 n Φ s x ↔ ∀ (i : ι), ContDiffWithinAt 𝕜 n (fun (x : E) => Φ x i) s x

theorem contDiffOn_pi {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {s : Set E} {n : WithTop ℕ∞} {ι : Type u_3} [Fintype ι] {F' : ι → Type u_5} [(i : ι) → NormedAddCommGroup (F' i)] [(i : ι) → NormedSpace 𝕜 (F' i)] {Φ : E → (i : ι) → F' i} : ContDiffOn 𝕜 n Φ s ↔ ∀ (i : ι), ContDiffOn 𝕜 n (fun (x : E) => Φ x i) s

theorem contDiffAt_pi {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {n : WithTop ℕ∞} {ι : Type u_3} [Fintype ι] {F' : ι → Type u_5} [(i : ι) → NormedAddCommGroup (F' i)] [(i : ι) → NormedSpace 𝕜 (F' i)] {Φ : E → (i : ι) → F' i} : ContDiffAt 𝕜 n Φ x ↔ ∀ (i : ι), ContDiffAt 𝕜 n (fun (x : E) => Φ x i) x

theorem contDiff_pi {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : WithTop ℕ∞} {ι : Type u_3} [Fintype ι] {F' : ι → Type u_5} [(i : ι) → NormedAddCommGroup (F' i)] [(i : ι) → NormedSpace 𝕜 (F' i)] {Φ : E → (i : ι) → F' i} : ContDiff 𝕜 n Φ ↔ ∀ (i : ι), ContDiff 𝕜 n fun (x : E) => Φ x i

theorem contDiff_pi' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : WithTop ℕ∞} {ι : Type u_3} [Fintype ι] {F' : ι → Type u_5} [(i : ι) → NormedAddCommGroup (F' i)] [(i : ι) → NormedSpace 𝕜 (F' i)] {Φ : E → (i : ι) → F' i} (hΦ : ∀ (i : ι), ContDiff 𝕜 n fun (x : E) => Φ x i) : ContDiff 𝕜 n Φ

theorem contDiffOn_pi' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {s : Set E} {n : WithTop ℕ∞} {ι : Type u_3} [Fintype ι] {F' : ι → Type u_5} [(i : ι) → NormedAddCommGroup (F' i)] [(i : ι) → NormedSpace 𝕜 (F' i)] {Φ : E → (i : ι) → F' i} (hΦ : ∀ (i : ι), ContDiffOn 𝕜 n (fun (x : E) => Φ x i) s) : ContDiffOn 𝕜 n Φ s

theorem contDiffAt_pi' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {n : WithTop ℕ∞} {ι : Type u_3} [Fintype ι] {F' : ι → Type u_5} [(i : ι) → NormedAddCommGroup (F' i)] [(i : ι) → NormedSpace 𝕜 (F' i)] {Φ : E → (i : ι) → F' i} (hΦ : ∀ (i : ι), ContDiffAt 𝕜 n (fun (x : E) => Φ x i) x) : ContDiffAt 𝕜 n Φ x

theorem contDiff_update {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {ι : Type u_3} [Fintype ι] {F' : ι → Type u_5} [(i : ι) → NormedAddCommGroup (F' i)] [(i : ι) → NormedSpace 𝕜 (F' i)] [DecidableEq ι] (k : WithTop ℕ∞) (x : (i : ι) → F' i) (i : ι) : ContDiff 𝕜 k (Function.update x i)

theorem contDiff_single {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {ι : Type u_3} [Fintype ι] (F' : ι → Type u_5) [(i : ι) → NormedAddCommGroup (F' i)] [(i : ι) → NormedSpace 𝕜 (F' i)] [DecidableEq ι] (k : WithTop ℕ∞) (i : ι) : ContDiff 𝕜 k (Pi.single i)

theorem contDiff_apply (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (E : Type uE) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : WithTop ℕ∞} {ι : Type u_3} [Fintype ι] (i : ι) : ContDiff 𝕜 n fun (f : ι → E) => f i

theorem contDiffAt_apply (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (E : Type uE) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : WithTop ℕ∞} {ι : Type u_3} [Fintype ι] (i : ι) (f : ι → E) : ContDiffAt 𝕜 n (fun (f : ι → E) => f i) f

theorem contDiffOn_apply (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (E : Type uE) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : WithTop ℕ∞} {ι : Type u_3} [Fintype ι] (i : ι) (s : Set (ι → E)) : ContDiffOn 𝕜 n (fun (f : ι → E) => f i) s

theorem contDiff_apply_apply (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (E : Type uE) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : WithTop ℕ∞} {ι : Type u_3} {ι' : Type u_4} [Fintype ι] [Fintype ι'] (i : ι) (j : ι') : ContDiff 𝕜 n fun (f : ι → ι' → E) => f i j

Sum of two functions

theorem HasFTaylorSeriesUpToOn.add {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} {f : E → F} {p : E → FormalMultilinearSeries 𝕜 E F} {n : WithTop ℕ∞} {q : E → FormalMultilinearSeries 𝕜 E F} {g : E → F} (hf : HasFTaylorSeriesUpToOn n f p s) (hg : HasFTaylorSeriesUpToOn n g q s) : HasFTaylorSeriesUpToOn n (f + g) (p + q) s

theorem contDiff_add {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} : ContDiff 𝕜 n fun (p : F × F) => p.1 + p.2

theorem ContDiffWithinAt.add {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x : E} {n : WithTop ℕ∞} {s : Set E} {f g : E → F} (hf : ContDiffWithinAt 𝕜 n f s x) (hg : ContDiffWithinAt 𝕜 n g s x) : ContDiffWithinAt 𝕜 n (fun (x : E) => f x + g x) s x

The sum of two C^n functions within a set at a point is C^n within this set at this point.

theorem ContDiffAt.add {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x : E} {n : WithTop ℕ∞} {f g : E → F} (hf : ContDiffAt 𝕜 n f x) (hg : ContDiffAt 𝕜 n g x) : ContDiffAt 𝕜 n (fun (x : E) => f x + g x) x

The sum of two C^n functions at a point is C^n at this point.

theorem ContDiff.add {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {f g : E → F} (hf : ContDiff 𝕜 n f) (hg : ContDiff 𝕜 n g) : ContDiff 𝕜 n fun (x : E) => f x + g x

The sum of two C^n functions is C^n.

theorem ContDiffOn.add {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {s : Set E} {f g : E → F} (hf : ContDiffOn 𝕜 n f s) (hg : ContDiffOn 𝕜 n g s) : ContDiffOn 𝕜 n (fun (x : E) => f x + g x) s

The sum of two C^n functions on a domain is C^n.

theorem iteratedFDerivWithin_add_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} {x : E} {i : ℕ} {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

The iterated derivative of the sum of two functions is the sum of the iterated derivatives.

theorem fun_iteratedFDerivWithin_add_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} {x : E} {i : ℕ} {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 (i : E) => f i + g i) s x = iteratedFDerivWithin 𝕜 i f s x + iteratedFDerivWithin 𝕜 i g s x

Eta-expanded form of iteratedFDerivWithin_add_apply

---

The iterated derivative of the sum of two functions is the sum of the iterated derivatives.

theorem iteratedFDeriv_add_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x : E} {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

theorem fun_iteratedFDeriv_add_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x : E} {i : ℕ} {f g : E → F} (hf : ContDiffAt 𝕜 (↑i) f x) (hg : ContDiffAt 𝕜 (↑i) g x) : iteratedFDeriv 𝕜 i (fun (i : E) => f i + g i) x = iteratedFDeriv 𝕜 i f x + iteratedFDeriv 𝕜 i g x

Eta-expanded form of iteratedFDeriv_add_apply

theorem iteratedFDeriv_add {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {i : ℕ} {f g : E → F} (hf : ContDiff 𝕜 (↑i) f) (hg : ContDiff 𝕜 (↑i) g) : iteratedFDeriv 𝕜 i (f + g) = iteratedFDeriv 𝕜 i f + iteratedFDeriv 𝕜 i g

theorem fun_iteratedFDeriv_add {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {i : ℕ} {f g : E → F} (hf : ContDiff 𝕜 (↑i) f) (hg : ContDiff 𝕜 (↑i) g) : (iteratedFDeriv 𝕜 i fun (i : E) => f i + g i) = fun (i_1 : E) => iteratedFDeriv 𝕜 i f i_1 + iteratedFDeriv 𝕜 i g i_1

Eta-expanded form of iteratedFDeriv_add

Negative

theorem contDiff_neg {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} : ContDiff 𝕜 n fun (p : F) => -p

theorem ContDiffWithinAt.neg {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x : E} {n : WithTop ℕ∞} {s : Set E} {f : E → F} (hf : ContDiffWithinAt 𝕜 n f s x) : ContDiffWithinAt 𝕜 n (fun (x : E) => -f x) s x

The negative of a C^n function within a domain at a point is C^n within this domain at this point.

theorem ContDiffAt.neg {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x : E} {n : WithTop ℕ∞} {f : E → F} (hf : ContDiffAt 𝕜 n f x) : ContDiffAt 𝕜 n (fun (x : E) => -f x) x

The negative of a C^n function at a point is C^n at this point.

theorem ContDiff.neg {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {f : E → F} (hf : ContDiff 𝕜 n f) : ContDiff 𝕜 n fun (x : E) => -f x

The negative of a C^n function is C^n.

theorem ContDiffOn.neg {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {s : Set E} {f : E → F} (hf : ContDiffOn 𝕜 n f s) : ContDiffOn 𝕜 n (fun (x : E) => -f x) s

The negative of a C^n function on a domain is C^n.

theorem iteratedFDerivWithin_neg_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} {x : E} {i : ℕ} {f : E → F} (hu : UniqueDiffOn 𝕜 s) (hx : x ∈ s) : iteratedFDerivWithin 𝕜 i (-f) s x = -iteratedFDerivWithin 𝕜 i f s x

theorem iteratedFDeriv_neg_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x : E} {i : ℕ} {f : E → F} : iteratedFDeriv 𝕜 i (-f) x = -iteratedFDeriv 𝕜 i f x

theorem iteratedFDeriv_neg {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {i : ℕ} {f : E → F} : iteratedFDeriv 𝕜 i (-f) = -iteratedFDeriv 𝕜 i f

Subtraction

theorem ContDiffWithinAt.sub {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x : E} {n : WithTop ℕ∞} {s : Set E} {f g : E → F} (hf : ContDiffWithinAt 𝕜 n f s x) (hg : ContDiffWithinAt 𝕜 n g s x) : ContDiffWithinAt 𝕜 n (fun (x : E) => f x - g x) s x

The difference of two C^n functions within a set at a point is C^n within this set at this point.

theorem ContDiffAt.sub {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x : E} {n : WithTop ℕ∞} {f g : E → F} (hf : ContDiffAt 𝕜 n f x) (hg : ContDiffAt 𝕜 n g x) : ContDiffAt 𝕜 n (fun (x : E) => f x - g x) x

The difference of two C^n functions at a point is C^n at this point.

theorem ContDiffOn.sub {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {s : Set E} {f g : E → F} (hf : ContDiffOn 𝕜 n f s) (hg : ContDiffOn 𝕜 n g s) : ContDiffOn 𝕜 n (fun (x : E) => f x - g x) s

The difference of two C^n functions on a domain is C^n.

theorem ContDiff.sub {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {f g : E → F} (hf : ContDiff 𝕜 n f) (hg : ContDiff 𝕜 n g) : ContDiff 𝕜 n fun (x : E) => f x - g x

The difference of two C^n functions is C^n.

theorem iteratedFDerivWithin_sub_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} {x : E} {i : ℕ} {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

The iterated derivative of the difference of two functions is the difference of the iterated derivatives.

theorem fun_iteratedFDerivWithin_sub_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} {x : E} {i : ℕ} {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 (i : E) => f i - g i) s x = iteratedFDerivWithin 𝕜 i f s x - iteratedFDerivWithin 𝕜 i g s x

Eta-expanded form of iteratedFDerivWithin_sub_apply

---

The iterated derivative of the difference of two functions is the difference of the iterated derivatives.

theorem iteratedFDeriv_sub_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x : E} {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

The iterated derivative of the difference of two functions is the difference of the iterated derivatives.

theorem fun_iteratedFDeriv_sub_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x : E} {i : ℕ} {f g : E → F} (hf : ContDiffAt 𝕜 (↑i) f x) (hg : ContDiffAt 𝕜 (↑i) g x) : iteratedFDeriv 𝕜 i (fun (i : E) => f i - g i) x = iteratedFDeriv 𝕜 i f x - iteratedFDeriv 𝕜 i g x

Eta-expanded form of iteratedFDeriv_sub_apply

---

The iterated derivative of the difference of two functions is the difference of the iterated derivatives.

theorem iteratedFDeriv_sub {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {i : ℕ} {f g : E → F} (hf : ContDiff 𝕜 (↑i) f) (hg : ContDiff 𝕜 (↑i) g) : iteratedFDeriv 𝕜 i (f - g) = iteratedFDeriv 𝕜 i f - iteratedFDeriv 𝕜 i g

The iterated derivative of the difference of two functions is the difference of the iterated derivatives.

theorem fun_iteratedFDeriv_sub {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {i : ℕ} {f g : E → F} (hf : ContDiff 𝕜 (↑i) f) (hg : ContDiff 𝕜 (↑i) g) : (iteratedFDeriv 𝕜 i fun (i : E) => f i - g i) = fun (i_1 : E) => iteratedFDeriv 𝕜 i f i_1 - iteratedFDeriv 𝕜 i g i_1

Eta-expanded form of iteratedFDeriv_sub

---

The iterated derivative of the difference of two functions is the difference of the iterated derivatives.

Sum of finitely many functions

theorem ContDiffWithinAt.sum {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {ι : Type u_3} {f : ι → E → F} {s : Finset ι} {t : Set E} {x : E} (h : ∀ i ∈ s, ContDiffWithinAt 𝕜 n (fun (x : E) => f i x) t x) : ContDiffWithinAt 𝕜 n (fun (x : E) => ∑ i ∈ s, f i x) t x

theorem ContDiffAt.sum {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {ι : Type u_3} {f : ι → E → F} {s : Finset ι} {x : E} (h : ∀ i ∈ s, ContDiffAt 𝕜 n (fun (x : E) => f i x) x) : ContDiffAt 𝕜 n (fun (x : E) => ∑ i ∈ s, f i x) x

theorem ContDiffOn.sum {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {ι : Type u_3} {f : ι → E → F} {s : Finset ι} {t : Set E} (h : ∀ i ∈ s, ContDiffOn 𝕜 n (fun (x : E) => f i x) t) : ContDiffOn 𝕜 n (fun (x : E) => ∑ i ∈ s, f i x) t

theorem ContDiff.sum {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {ι : Type u_3} {f : ι → E → F} {s : Finset ι} (h : ∀ i ∈ s, ContDiff 𝕜 n fun (x : E) => f i x) : ContDiff 𝕜 n fun (x : E) => ∑ i ∈ s, f i x

theorem iteratedFDerivWithin_sum_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} {ι : Type u_3} {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

theorem iteratedFDerivWithin_fun_sum_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} {ι : Type u_3} {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 (fun (z : E) => ∑ j ∈ u, f j z) s x = ∑ j ∈ u, iteratedFDerivWithin 𝕜 i (f j) s x

theorem iteratedFDeriv_sum_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {ι : Type u_3} {f : ι → E → F} {u : Finset ι} {n : ℕ} {x : E} (h : ∀ j ∈ u, ContDiffAt 𝕜 (↑n) (f j) x) : iteratedFDeriv 𝕜 n (∑ j ∈ u, f j) x = ∑ j ∈ u, iteratedFDeriv 𝕜 n (f j) x

theorem iteratedFDeriv_fun_sum_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {ι : Type u_3} {f : ι → E → F} {u : Finset ι} {n : ℕ} {x : E} (h : ∀ j ∈ u, ContDiffAt 𝕜 (↑n) (f j) x) : iteratedFDeriv 𝕜 n (fun (z : E) => ∑ j ∈ u, f j z) x = ∑ j ∈ u, iteratedFDeriv 𝕜 n (f j) x

theorem iteratedFDeriv_sum {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {ι : Type u_3} {f : ι → E → F} {u : Finset ι} {i : ℕ} (h : ∀ j ∈ u, ContDiff 𝕜 (↑i) (f j)) : (iteratedFDeriv 𝕜 i fun (x : E) => ∑ j ∈ u, f j x) = ∑ j ∈ u, iteratedFDeriv 𝕜 i (f j)

Product of two functions

theorem contDiff_mul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {𝔸 : Type u_3} [NormedRing 𝔸] [NormedAlgebra 𝕜 𝔸] : ContDiff 𝕜 n fun (p : 𝔸 × 𝔸) => p.1 * p.2

theorem ContDiffWithinAt.mul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {n : WithTop ℕ∞} {𝔸 : Type u_3} [NormedRing 𝔸] [NormedAlgebra 𝕜 𝔸] {s : Set E} {f g : E → 𝔸} (hf : ContDiffWithinAt 𝕜 n f s x) (hg : ContDiffWithinAt 𝕜 n g s x) : ContDiffWithinAt 𝕜 n (fun (x : E) => f x * g x) s x

The product of two C^n functions within a set at a point is C^n within this set at this point.

theorem ContDiffAt.mul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {n : WithTop ℕ∞} {𝔸 : Type u_3} [NormedRing 𝔸] [NormedAlgebra 𝕜 𝔸] {f g : E → 𝔸} (hf : ContDiffAt 𝕜 n f x) (hg : ContDiffAt 𝕜 n g x) : ContDiffAt 𝕜 n (fun (x : E) => f x * g x) x

The product of two C^n functions at a point is C^n at this point.

theorem ContDiffOn.mul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {s : Set E} {n : WithTop ℕ∞} {𝔸 : Type u_3} [NormedRing 𝔸] [NormedAlgebra 𝕜 𝔸] {f g : E → 𝔸} (hf : ContDiffOn 𝕜 n f s) (hg : ContDiffOn 𝕜 n g s) : ContDiffOn 𝕜 n (fun (x : E) => f x * g x) s

The product of two C^n functions on a domain is C^n.

theorem ContDiff.mul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : WithTop ℕ∞} {𝔸 : Type u_3} [NormedRing 𝔸] [NormedAlgebra 𝕜 𝔸] {f g : E → 𝔸} (hf : ContDiff 𝕜 n f) (hg : ContDiff 𝕜 n g) : ContDiff 𝕜 n fun (x : E) => f x * g x

The product of two C^n functions is C^n.

theorem contDiffWithinAt_prod' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {s : Set E} {x : E} {n : WithTop ℕ∞} {𝔸' : Type u_4} {ι : Type u_5} [NormedCommRing 𝔸'] [NormedAlgebra 𝕜 𝔸'] {t : Finset ι} {f : ι → E → 𝔸'} (h : ∀ i ∈ t, ContDiffWithinAt 𝕜 n (f i) s x) : ContDiffWithinAt 𝕜 n (∏ i ∈ t, f i) s x

theorem contDiffWithinAt_prod {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {s : Set E} {x : E} {n : WithTop ℕ∞} {𝔸' : Type u_4} {ι : Type u_5} [NormedCommRing 𝔸'] [NormedAlgebra 𝕜 𝔸'] {t : Finset ι} {f : ι → E → 𝔸'} (h : ∀ i ∈ t, ContDiffWithinAt 𝕜 n (f i) s x) : ContDiffWithinAt 𝕜 n (fun (y : E) => ∏ i ∈ t, f i y) s x

theorem contDiffAt_prod' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {n : WithTop ℕ∞} {𝔸' : Type u_4} {ι : Type u_5} [NormedCommRing 𝔸'] [NormedAlgebra 𝕜 𝔸'] {t : Finset ι} {f : ι → E → 𝔸'} (h : ∀ i ∈ t, ContDiffAt 𝕜 n (f i) x) : ContDiffAt 𝕜 n (∏ i ∈ t, f i) x

theorem contDiffAt_prod {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {n : WithTop ℕ∞} {𝔸' : Type u_4} {ι : Type u_5} [NormedCommRing 𝔸'] [NormedAlgebra 𝕜 𝔸'] {t : Finset ι} {f : ι → E → 𝔸'} (h : ∀ i ∈ t, ContDiffAt 𝕜 n (f i) x) : ContDiffAt 𝕜 n (fun (y : E) => ∏ i ∈ t, f i y) x

theorem contDiffOn_prod' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {s : Set E} {n : WithTop ℕ∞} {𝔸' : Type u_4} {ι : Type u_5} [NormedCommRing 𝔸'] [NormedAlgebra 𝕜 𝔸'] {t : Finset ι} {f : ι → E → 𝔸'} (h : ∀ i ∈ t, ContDiffOn 𝕜 n (f i) s) : ContDiffOn 𝕜 n (∏ i ∈ t, f i) s

theorem contDiffOn_prod {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {s : Set E} {n : WithTop ℕ∞} {𝔸' : Type u_4} {ι : Type u_5} [NormedCommRing 𝔸'] [NormedAlgebra 𝕜 𝔸'] {t : Finset ι} {f : ι → E → 𝔸'} (h : ∀ i ∈ t, ContDiffOn 𝕜 n (f i) s) : ContDiffOn 𝕜 n (fun (y : E) => ∏ i ∈ t, f i y) s

theorem contDiff_prod' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : WithTop ℕ∞} {𝔸' : Type u_4} {ι : Type u_5} [NormedCommRing 𝔸'] [NormedAlgebra 𝕜 𝔸'] {t : Finset ι} {f : ι → E → 𝔸'} (h : ∀ i ∈ t, ContDiff 𝕜 n (f i)) : ContDiff 𝕜 n (∏ i ∈ t, f i)

theorem contDiff_prod {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : WithTop ℕ∞} {𝔸' : Type u_4} {ι : Type u_5} [NormedCommRing 𝔸'] [NormedAlgebra 𝕜 𝔸'] {t : Finset ι} {f : ι → E → 𝔸'} (h : ∀ i ∈ t, ContDiff 𝕜 n (f i)) : ContDiff 𝕜 n fun (y : E) => ∏ i ∈ t, f i y

theorem ContDiff.pow {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : WithTop ℕ∞} {𝔸 : Type u_3} [NormedRing 𝔸] [NormedAlgebra 𝕜 𝔸] {f : E → 𝔸} (hf : ContDiff 𝕜 n f) (m : ℕ) : ContDiff 𝕜 n fun (x : E) => f x ^ m

theorem ContDiffWithinAt.pow {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {s : Set E} {x : E} {n : WithTop ℕ∞} {𝔸 : Type u_3} [NormedRing 𝔸] [NormedAlgebra 𝕜 𝔸] {f : E → 𝔸} (hf : ContDiffWithinAt 𝕜 n f s x) (m : ℕ) : ContDiffWithinAt 𝕜 n (fun (y : E) => f y ^ m) s x

theorem ContDiffAt.pow {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {n : WithTop ℕ∞} {𝔸 : Type u_3} [NormedRing 𝔸] [NormedAlgebra 𝕜 𝔸] {f : E → 𝔸} (hf : ContDiffAt 𝕜 n f x) (m : ℕ) : ContDiffAt 𝕜 n (fun (y : E) => f y ^ m) x

theorem ContDiffOn.pow {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {s : Set E} {n : WithTop ℕ∞} {𝔸 : Type u_3} [NormedRing 𝔸] [NormedAlgebra 𝕜 𝔸] {f : E → 𝔸} (hf : ContDiffOn 𝕜 n f s) (m : ℕ) : ContDiffOn 𝕜 n (fun (y : E) => f y ^ m) s

theorem ContDiffWithinAt.div_const {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {s : Set E} {x : E} {𝕜' : Type u_6} [NormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {f : E → 𝕜'} {n : WithTop ℕ∞} (hf : ContDiffWithinAt 𝕜 n f s x) (c : 𝕜') : ContDiffWithinAt 𝕜 n (fun (x : E) => f x / c) s x

theorem ContDiffAt.div_const {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {𝕜' : Type u_6} [NormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {f : E → 𝕜'} {n : WithTop ℕ∞} (hf : ContDiffAt 𝕜 n f x) (c : 𝕜') : ContDiffAt 𝕜 n (fun (x : E) => f x / c) x

theorem ContDiffOn.div_const {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {s : Set E} {𝕜' : Type u_6} [NormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {f : E → 𝕜'} {n : WithTop ℕ∞} (hf : ContDiffOn 𝕜 n f s) (c : 𝕜') : ContDiffOn 𝕜 n (fun (x : E) => f x / c) s

theorem ContDiff.div_const {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {𝕜' : Type u_6} [NormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {f : E → 𝕜'} {n : WithTop ℕ∞} (hf : ContDiff 𝕜 n f) (c : 𝕜') : ContDiff 𝕜 n fun (x : E) => f x / c

Scalar multiplication

theorem contDiff_smul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {𝕜' : Type u_3} [NormedRing 𝕜'] [NormedAlgebra 𝕜 𝕜'] [Module 𝕜' F] [IsBoundedSMul 𝕜' F] [IsScalarTower 𝕜 𝕜' F] : ContDiff 𝕜 n fun (p : 𝕜' × F) => p.1 • p.2

theorem ContDiffWithinAt.smul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x : E} {n : WithTop ℕ∞} {𝕜' : Type u_3} [NormedRing 𝕜'] [NormedAlgebra 𝕜 𝕜'] [Module 𝕜' F] [IsBoundedSMul 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {s : Set E} {f : E → 𝕜'} {g : E → F} (hf : ContDiffWithinAt 𝕜 n f s x) (hg : ContDiffWithinAt 𝕜 n g s x) : ContDiffWithinAt 𝕜 n (f • g) s x

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.fun_smul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x : E} {n : WithTop ℕ∞} {𝕜' : Type u_3} [NormedRing 𝕜'] [NormedAlgebra 𝕜 𝕜'] [Module 𝕜' F] [IsBoundedSMul 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {s : Set E} {f : E → 𝕜'} {g : E → F} (hf : ContDiffWithinAt 𝕜 n f s x) (hg : ContDiffWithinAt 𝕜 n g s x) : ContDiffWithinAt 𝕜 n (fun (i : E) => f i • g i) s x

Eta-expanded form of ContDiffWithinAt.smul

---

The scalar multiplication of two C^n functions within a set at a point is C^n within this set at this point.

theorem ContDiffAt.smul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x : E} {n : WithTop ℕ∞} {𝕜' : Type u_3} [NormedRing 𝕜'] [NormedAlgebra 𝕜 𝕜'] [Module 𝕜' F] [IsBoundedSMul 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {f : E → 𝕜'} {g : E → F} (hf : ContDiffAt 𝕜 n f x) (hg : ContDiffAt 𝕜 n g x) : ContDiffAt 𝕜 n (f • g) x

The scalar multiplication of two C^n functions at a point is C^n at this point.

theorem ContDiffAt.fun_smul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x : E} {n : WithTop ℕ∞} {𝕜' : Type u_3} [NormedRing 𝕜'] [NormedAlgebra 𝕜 𝕜'] [Module 𝕜' F] [IsBoundedSMul 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {f : E → 𝕜'} {g : E → F} (hf : ContDiffAt 𝕜 n f x) (hg : ContDiffAt 𝕜 n g x) : ContDiffAt 𝕜 n (fun (i : E) => f i • g i) x

Eta-expanded form of ContDiffAt.smul

---

The scalar multiplication of two C^n functions at a point is C^n at this point.

theorem ContDiff.smul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {𝕜' : Type u_3} [NormedRing 𝕜'] [NormedAlgebra 𝕜 𝕜'] [Module 𝕜' F] [IsBoundedSMul 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {f : E → 𝕜'} {g : E → F} (hf : ContDiff 𝕜 n f) (hg : ContDiff 𝕜 n g) : ContDiff 𝕜 n (f • g)

The scalar multiplication of two C^n functions is C^n.

theorem ContDiff.fun_smul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {𝕜' : Type u_3} [NormedRing 𝕜'] [NormedAlgebra 𝕜 𝕜'] [Module 𝕜' F] [IsBoundedSMul 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {f : E → 𝕜'} {g : E → F} (hf : ContDiff 𝕜 n f) (hg : ContDiff 𝕜 n g) : ContDiff 𝕜 n fun (i : E) => f i • g i

Eta-expanded form of ContDiff.smul

---

The scalar multiplication of two C^n functions is C^n.

theorem ContDiffOn.smul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {𝕜' : Type u_3} [NormedRing 𝕜'] [NormedAlgebra 𝕜 𝕜'] [Module 𝕜' F] [IsBoundedSMul 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {s : Set E} {f : E → 𝕜'} {g : E → F} (hf : ContDiffOn 𝕜 n f s) (hg : ContDiffOn 𝕜 n g s) : ContDiffOn 𝕜 n (f • g) s

The scalar multiplication of two C^n functions on a domain is C^n.

theorem ContDiffOn.fun_smul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {𝕜' : Type u_3} [NormedRing 𝕜'] [NormedAlgebra 𝕜 𝕜'] [Module 𝕜' F] [IsBoundedSMul 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {s : Set E} {f : E → 𝕜'} {g : E → F} (hf : ContDiffOn 𝕜 n f s) (hg : ContDiffOn 𝕜 n g s) : ContDiffOn 𝕜 n (fun (i : E) => f i • g i) s

Eta-expanded form of ContDiffOn.smul

---

The scalar multiplication of two C^n functions on a domain is C^n.

Constant scalar multiplication

TODO: generalize results in this section -- if c is a unit (or R is a group), then one can drop ContDiff* assumptions in some lemmas about iteratedFDeriv and iteratedFDerivWithin.

theorem contDiff_const_smul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {R : Type u_3} [DistribSMul R F] [SMulCommClass 𝕜 R F] [ContinuousConstSMul R F] (c : R) : ContDiff 𝕜 n fun (p : F) => c • p

Scalar multiplication is smooth (as a function of the vector variable).

theorem contDiff_smul_const {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {A : Type u_4} [NormedRing A] [NormedAlgebra 𝕜 A] [Module A F] [IsScalarTower 𝕜 A F] [IsBoundedSMul A F] (v : F) : ContDiff 𝕜 n fun (a : A) => a • v

Scalar multiplication is smooth (as a function of the scalar variable).

theorem ContDiffWithinAt.const_smul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {R : Type u_3} [DistribSMul R F] [SMulCommClass 𝕜 R F] [ContinuousConstSMul R F] {s : Set E} {f : E → F} {x : E} (c : R) (hf : ContDiffWithinAt 𝕜 n f s x) : ContDiffWithinAt 𝕜 n (fun (y : E) => c • f y) s x

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.smul_const {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {A : Type u_4} [NormedRing A] [NormedAlgebra 𝕜 A] [Module A F] [IsScalarTower 𝕜 A F] [IsBoundedSMul A F] {s : Set E} {f : E → A} {x : E} (hf : ContDiffWithinAt 𝕜 n f s x) (v : F) : ContDiffWithinAt 𝕜 n (fun (y : E) => f y • v) s x

The scalar multiplication of C^n function within a set at a point and a constant and is C^n within this set at this point.

theorem ContDiffAt.const_smul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {R : Type u_3} [DistribSMul R F] [SMulCommClass 𝕜 R F] [ContinuousConstSMul R F] {f : E → F} {x : E} (c : R) (hf : ContDiffAt 𝕜 n f x) : ContDiffAt 𝕜 n (fun (y : E) => c • f y) x

The scalar multiplication of a constant and a C^n function at a point is C^n at this point.

theorem ContDiffAt.smul_const {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {A : Type u_4} [NormedRing A] [NormedAlgebra 𝕜 A] [Module A F] [IsScalarTower 𝕜 A F] [IsBoundedSMul A F] {f : E → A} {x : E} (hf : ContDiffAt 𝕜 n f x) (v : F) : ContDiffAt 𝕜 n (fun (y : E) => f y • v) x

The scalar multiplication of a C^n function at a point and a constant is C^n at this point.

theorem ContDiff.const_smul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {R : Type u_3} [DistribSMul R F] [SMulCommClass 𝕜 R F] [ContinuousConstSMul R F] {f : E → F} (c : R) (hf : ContDiff 𝕜 n f) : ContDiff 𝕜 n fun (y : E) => c • f y

The scalar multiplication of a constant and a C^n function is C^n.

theorem ContDiff.smul_const {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {A : Type u_4} [NormedRing A] [NormedAlgebra 𝕜 A] [Module A F] [IsScalarTower 𝕜 A F] [IsBoundedSMul A F] {f : E → A} (hf : ContDiff 𝕜 n f) (v : F) : ContDiff 𝕜 n fun (y : E) => f y • v

The scalar multiplication of a C^n function and a constant is C^n.

theorem ContDiffOn.const_smul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {R : Type u_3} [DistribSMul R F] [SMulCommClass 𝕜 R F] [ContinuousConstSMul R F] {s : Set E} {f : E → F} (c : R) (hf : ContDiffOn 𝕜 n f s) : ContDiffOn 𝕜 n (fun (y : E) => c • f y) s

The scalar multiplication of a constant and a C^n function on a domain is C^n.

theorem ContDiffOn.smul_const {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {A : Type u_4} [NormedRing A] [NormedAlgebra 𝕜 A] [Module A F] [IsScalarTower 𝕜 A F] [IsBoundedSMul A F] {s : Set E} {f : E → A} (hf : ContDiffOn 𝕜 n f s) (v : F) : ContDiffOn 𝕜 n (fun (y : E) => f y • v) s

The scalar multiplication of a C^n function on a domain and a constant is C^n.

theorem iteratedFDerivWithin_const_smul_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} {f : E → F} {x : E} {R : Type u_3} [DistribSMul R F] [SMulCommClass 𝕜 R F] [ContinuousConstSMul R F] {i : ℕ} {a : R} (hf : ContDiffWithinAt 𝕜 (↑i) f s x) (hu : UniqueDiffOn 𝕜 s) (hx : x ∈ s) : iteratedFDerivWithin 𝕜 i (a • f) s x = a • iteratedFDerivWithin 𝕜 i f s x

theorem iteratedFDerivWithin_smul_const_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} {x : E} {A : Type u_4} [NormedRing A] [NormedAlgebra 𝕜 A] [Module A F] [IsScalarTower 𝕜 A F] [IsBoundedSMul A F] {i : ℕ} {v : F} {f : E → A} (hf : ContDiffWithinAt 𝕜 (↑i) f s x) (hu : UniqueDiffOn 𝕜 s) (hx : x ∈ s) : iteratedFDerivWithin 𝕜 i (fun (y : E) => f y • v) s x = ((ContinuousLinearMap.id 𝕜 A).smulRight v).compContinuousMultilinearMap (iteratedFDerivWithin 𝕜 i f s x)

theorem iteratedFDeriv_const_smul_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {x : E} {R : Type u_3} [DistribSMul R F] [SMulCommClass 𝕜 R F] [ContinuousConstSMul R F] {i : ℕ} {a : R} (hf : ContDiffAt 𝕜 (↑i) f x) : iteratedFDeriv 𝕜 i (a • f) x = a • iteratedFDeriv 𝕜 i f x

theorem iteratedFDeriv_const_smul_apply' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {x : E} {R : Type u_3} [DistribSMul R F] [SMulCommClass 𝕜 R F] [ContinuousConstSMul R F] {i : ℕ} {a : R} (hf : ContDiffAt 𝕜 (↑i) f x) : iteratedFDeriv 𝕜 i (fun (x : E) => a • f x) x = a • iteratedFDeriv 𝕜 i f x

theorem iteratedFDeriv_smul_const_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x : E} {A : Type u_4} [NormedRing A] [NormedAlgebra 𝕜 A] [Module A F] [IsScalarTower 𝕜 A F] [IsBoundedSMul A F] {i : ℕ} {v : F} {f : E → A} (hf : ContDiffAt 𝕜 (↑i) f x) : iteratedFDeriv 𝕜 i (fun (y : E) => f y • v) x = ((ContinuousLinearMap.id 𝕜 A).smulRight v).compContinuousMultilinearMap (iteratedFDeriv 𝕜 i f x)

theorem iteratedFDeriv_comp_const_smul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {i : ℕ} (a : 𝕜) (hf : ContDiff 𝕜 (↑i) f) : (iteratedFDeriv 𝕜 i fun (z : E) => f (a • z)) = fun (x : E) => a ^ i • iteratedFDeriv 𝕜 i f (a • x)

Cartesian product of two functions

theorem ContDiffWithinAt.prodMap' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {F' : Type u_4} [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] {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

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 {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {F' : Type u_4} [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] {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)

theorem ContDiffOn.prodMap {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {F' : Type u_6} [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)

The product map of two C^n functions on a set is C^n on the product set.

theorem ContDiffAt.prodMap {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {F' : Type u_4} [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] {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)

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' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {F' : Type u_4} [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] {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

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 ContDiff.prodMap {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {F' : Type u_4} [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] {f : E → F} {g : E' → F'} (hf : ContDiff 𝕜 n f) (hg : ContDiff 𝕜 n g) : ContDiff 𝕜 n (Prod.map f g)

The product map of two C^n functions is C^n.

theorem contDiff_prodMk_left {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} (f₀ : F) : ContDiff 𝕜 n fun (e : E) => (e, f₀)

theorem contDiff_prodMk_right {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} (e₀ : E) : ContDiff 𝕜 n fun (f : F) => (e₀, f)

Inversion in a complete normed algebra (or more generally with summable geometric series)

theorem contDiffAt_ringInverse (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {R : Type u_3} [NormedRing R] [NormedAlgebra 𝕜 R] [HasSummableGeomSeries R] (x : Rˣ) : ContDiffAt 𝕜 n Ring.inverse ↑x

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_inv (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {𝕜' : Type u_4} [NormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {x : 𝕜'} (hx : x ≠ 0) {n : WithTop ℕ∞} : ContDiffAt 𝕜 n Inv.inv x

theorem contDiffOn_inv (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {𝕜' : Type u_4} [NormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {n : WithTop ℕ∞} : ContDiffOn 𝕜 n Inv.inv {0}ᶜ

theorem ContDiffWithinAt.inv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {s : Set E} {x : E} {𝕜' : Type u_4} [NormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {f : E → 𝕜'} {n : WithTop ℕ∞} (hf : ContDiffWithinAt 𝕜 n f s x) (hx : f x ≠ 0) : ContDiffWithinAt 𝕜 n f⁻¹ s x

theorem ContDiffWithinAt.fun_inv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {s : Set E} {x : E} {𝕜' : Type u_4} [NormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {f : E → 𝕜'} {n : WithTop ℕ∞} (hf : ContDiffWithinAt 𝕜 n f s x) (hx : f x ≠ 0) : ContDiffWithinAt 𝕜 n (fun (i : E) => (f i)⁻¹) s x

Eta-expanded form of ContDiffWithinAt.inv

theorem ContDiffOn.inv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {s : Set E} {n : WithTop ℕ∞} {𝕜' : Type u_4} [NormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {f : E → 𝕜'} (hf : ContDiffOn 𝕜 n f s) (h : ∀ x ∈ s, f x ≠ 0) : ContDiffOn 𝕜 n f⁻¹ s

theorem ContDiffOn.fun_inv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {s : Set E} {n : WithTop ℕ∞} {𝕜' : Type u_4} [NormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {f : E → 𝕜'} (hf : ContDiffOn 𝕜 n f s) (h : ∀ x ∈ s, f x ≠ 0) : ContDiffOn 𝕜 n (fun (i : E) => (f i)⁻¹) s

Eta-expanded form of ContDiffOn.inv

theorem ContDiffAt.inv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {n : WithTop ℕ∞} {𝕜' : Type u_4} [NormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {f : E → 𝕜'} (hf : ContDiffAt 𝕜 n f x) (hx : f x ≠ 0) : ContDiffAt 𝕜 n f⁻¹ x

theorem ContDiffAt.fun_inv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {n : WithTop ℕ∞} {𝕜' : Type u_4} [NormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {f : E → 𝕜'} (hf : ContDiffAt 𝕜 n f x) (hx : f x ≠ 0) : ContDiffAt 𝕜 n (fun (i : E) => (f i)⁻¹) x

Eta-expanded form of ContDiffAt.inv

theorem ContDiff.inv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : WithTop ℕ∞} {𝕜' : Type u_4} [NormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {f : E → 𝕜'} (hf : ContDiff 𝕜 n f) (h : ∀ (x : E), f x ≠ 0) : ContDiff 𝕜 n f⁻¹

theorem ContDiff.fun_inv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : WithTop ℕ∞} {𝕜' : Type u_4} [NormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {f : E → 𝕜'} (hf : ContDiff 𝕜 n f) (h : ∀ (x : E), f x ≠ 0) : ContDiff 𝕜 n fun (i : E) => (f i)⁻¹

Eta-expanded form of ContDiff.inv

theorem ContDiffWithinAt.div {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {s : Set E} {x : E} {f g : E → 𝕜} {n : WithTop ℕ∞} (hf : ContDiffWithinAt 𝕜 n f s x) (hg : ContDiffWithinAt 𝕜 n g s x) (hx : g x ≠ 0) : ContDiffWithinAt 𝕜 n (f / g) s x

theorem ContDiffWithinAt.fun_div {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {s : Set E} {x : E} {f g : E → 𝕜} {n : WithTop ℕ∞} (hf : ContDiffWithinAt 𝕜 n f s x) (hg : ContDiffWithinAt 𝕜 n g s x) (hx : g x ≠ 0) : ContDiffWithinAt 𝕜 n (fun (i : E) => f i / g i) s x

Eta-expanded form of ContDiffWithinAt.div

theorem ContDiffOn.div {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {s : Set E} {f g : E → 𝕜} {n : WithTop ℕ∞} (hf : ContDiffOn 𝕜 n f s) (hg : ContDiffOn 𝕜 n g s) (h₀ : ∀ x ∈ s, g x ≠ 0) : ContDiffOn 𝕜 n (f / g) s

theorem ContDiffOn.fun_div {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {s : Set E} {f g : E → 𝕜} {n : WithTop ℕ∞} (hf : ContDiffOn 𝕜 n f s) (hg : ContDiffOn 𝕜 n g s) (h₀ : ∀ x ∈ s, g x ≠ 0) : ContDiffOn 𝕜 n (fun (i : E) => f i / g i) s

Eta-expanded form of ContDiffOn.div

theorem ContDiffAt.div {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {f g : E → 𝕜} {n : WithTop ℕ∞} (hf : ContDiffAt 𝕜 n f x) (hg : ContDiffAt 𝕜 n g x) (hx : g x ≠ 0) : ContDiffAt 𝕜 n (f / g) x

theorem ContDiffAt.fun_div {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {f g : E → 𝕜} {n : WithTop ℕ∞} (hf : ContDiffAt 𝕜 n f x) (hg : ContDiffAt 𝕜 n g x) (hx : g x ≠ 0) : ContDiffAt 𝕜 n (fun (i : E) => f i / g i) x

Eta-expanded form of ContDiffAt.div

theorem ContDiff.div {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f g : E → 𝕜} {n : WithTop ℕ∞} (hf : ContDiff 𝕜 n f) (hg : ContDiff 𝕜 n g) (h0 : ∀ (x : E), g x ≠ 0) : ContDiff 𝕜 n (f / g)

theorem ContDiff.fun_div {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f g : E → 𝕜} {n : WithTop ℕ∞} (hf : ContDiff 𝕜 n f) (hg : ContDiff 𝕜 n g) (h0 : ∀ (x : E), g x ≠ 0) : ContDiff 𝕜 n fun (i : E) => f i / g i

Eta-expanded form of ContDiff.div

Inversion of continuous linear maps between Banach spaces

theorem contDiffAt_map_inverse {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} [CompleteSpace E] (e : E ≃L[𝕜] F) : ContDiffAt 𝕜 n ContinuousLinearMap.inverse ↑e

At a continuous linear equivalence e : E ≃L[𝕜] F between Banach spaces, the operation of inversion is C^n, for all n.

theorem ContinuousLinearMap.IsInvertible.contDiffAt_map_inverse {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} [CompleteSpace E] {e : E →L[𝕜] F} (he : e.IsInvertible) : ContDiffAt 𝕜 n inverse e

At an invertible map e : M →L[R] M₂ between Banach spaces, the operation of inversion is C^n, for all n.

theorem OpenPartialHomeomorph.contDiffAt_symm {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} [CompleteSpace E] (f : OpenPartialHomeomorph E F) {f₀' : E ≃L[𝕜] F} {a : F} (ha : a ∈ f.target) (hf₀' : HasFDerivAt (↑f) (↑f₀') (↑f.symm a)) (hf : ContDiffAt 𝕜 n (↑f) (↑f.symm a)) : ContDiffAt 𝕜 n (↑f.symm) a

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 Homeomorph.contDiff_symm {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} [CompleteSpace E] (f : E ≃ₜ F) {f₀' : E → E ≃L[𝕜] F} (hf₀' : ∀ (a : E), HasFDerivAt (⇑f) (↑(f₀' a)) a) (hf : ContDiff 𝕜 n ⇑f) : ContDiff 𝕜 n ⇑f.symm

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 OpenPartialHomeomorph.contDiffAt_symm_deriv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} [CompleteSpace 𝕜] (f : OpenPartialHomeomorph 𝕜 𝕜) {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

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 Homeomorph.contDiff_symm_deriv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} [CompleteSpace 𝕜] (f : 𝕜 ≃ₜ 𝕜) {f' : 𝕜 → 𝕜} (h₀ : ∀ (x : 𝕜), f' x ≠ 0) (hf' : ∀ (x : 𝕜), HasDerivAt (⇑f) (f' x) x) (hf : ContDiff 𝕜 n ⇑f) : ContDiff 𝕜 n ⇑f.symm

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.

def OpenPartialHomeomorph.restrContDiff (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : OpenPartialHomeomorph E F) (n : WithTop ℕ∞) (hn : n ≠ ↑⊤) : OpenPartialHomeomorph E F

Restrict an open 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.

@[simp]

theorem OpenPartialHomeomorph.restrContDiff_target (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : OpenPartialHomeomorph E F) (n : WithTop ℕ∞) (hn : n ≠ ↑⊤) : (restrContDiff 𝕜 f n hn).target = f.target ∩ {y : F | ContDiffAt 𝕜 n (↑f.symm) y ∧ ContDiffAt 𝕜 n (↑f) (↑f.symm y)}

@[simp]

theorem OpenPartialHomeomorph.restrContDiff_apply (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : OpenPartialHomeomorph E F) (n : WithTop ℕ∞) (hn : n ≠ ↑⊤) (a✝ : E) : ↑(restrContDiff 𝕜 f n hn) a✝ = ↑f a✝

@[simp]

theorem OpenPartialHomeomorph.restrContDiff_source (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : OpenPartialHomeomorph E F) (n : WithTop ℕ∞) (hn : n ≠ ↑⊤) : (restrContDiff 𝕜 f n hn).source = f.source ∩ {x : E | ContDiffAt 𝕜 n (↑f) x ∧ ContDiffAt 𝕜 n (↑f.symm) (↑f x)}

@[simp]

theorem OpenPartialHomeomorph.restrContDiff_symm_apply (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : OpenPartialHomeomorph E F) (n : WithTop ℕ∞) (hn : n ≠ ↑⊤) (a✝ : F) : ↑(restrContDiff 𝕜 f n hn).symm a✝ = ↑f.symm a✝

theorem OpenPartialHomeomorph.contDiffOn_restrContDiff_source (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : OpenPartialHomeomorph E F) {n : WithTop ℕ∞} (hn : n ≠ ↑⊤) : ContDiffOn 𝕜 n (↑f) (restrContDiff 𝕜 f n hn).source

theorem OpenPartialHomeomorph.contDiffOn_restrContDiff_target (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : OpenPartialHomeomorph E F) {n : WithTop ℕ∞} (hn : n ≠ ↑⊤) : ContDiffOn 𝕜 n (↑f.symm) (restrContDiff 𝕜 f n hn).target

Restricting from ℂ to ℝ, or generally from 𝕜' to 𝕜

If a function is n times continuously differentiable over ℂ, then it is n times continuously differentiable over ℝ. In this paragraph, we give variants of this statement, in the general situation where ℂ and ℝ are replaced respectively by 𝕜' and 𝕜 where 𝕜' is a normed algebra over 𝕜.

theorem HasFTaylorSeriesUpToOn.restrictScalars (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} {f : E → F} {𝕜' : Type u_3} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] [NormedSpace 𝕜' E] [IsScalarTower 𝕜 𝕜' E] [NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {p' : E → FormalMultilinearSeries 𝕜' E F} {n : WithTop ℕ∞} (h : HasFTaylorSeriesUpToOn n f p' s) : HasFTaylorSeriesUpToOn n f (fun (x : E) => FormalMultilinearSeries.restrictScalars 𝕜 (p' x)) s

theorem ContDiffWithinAt.restrict_scalars (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} {f : E → F} {x : E} {n : WithTop ℕ∞} {𝕜' : Type u_3} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] [NormedSpace 𝕜' E] [IsScalarTower 𝕜 𝕜' E] [NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F] (h : ContDiffWithinAt 𝕜' n f s x) : ContDiffWithinAt 𝕜 n f s x

theorem ContDiffOn.restrict_scalars (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} {f : E → F} {n : WithTop ℕ∞} {𝕜' : Type u_3} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] [NormedSpace 𝕜' E] [IsScalarTower 𝕜 𝕜' E] [NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F] (h : ContDiffOn 𝕜' n f s) : ContDiffOn 𝕜 n f s

theorem ContDiffAt.restrict_scalars (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {x : E} {n : WithTop ℕ∞} {𝕜' : Type u_3} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] [NormedSpace 𝕜' E] [IsScalarTower 𝕜 𝕜' E] [NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F] (h : ContDiffAt 𝕜' n f x) : ContDiffAt 𝕜 n f x

theorem ContDiff.restrict_scalars (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {n : WithTop ℕ∞} {𝕜' : Type u_3} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] [NormedSpace 𝕜' E] [IsScalarTower 𝕜 𝕜' E] [NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F] (h : ContDiff 𝕜' n f) : ContDiff 𝕜 n f