Higher differentiability of usual operations #
We prove that the usual operations (addition, multiplication, difference, composition, and
so on) preserve C^n functions.
Notations #
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 ∞ and ⊤ : WithTop ℕ∞ 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}
:
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}
:
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}
:
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}
:
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 : ι)
:
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
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 ℕ∞}
:
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)
:
The sum of two C^nfunctions 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.
See also iteratedFDerivWithin_add_apply', which uses the spelling (fun x ↦ f x + g x)
instead of f + g.
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 (fun (x : E) => f x + g x) 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.
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
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)
:
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)
:
Negative #
theorem
contDiff_neg
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{n : WithTop ℕ∞}
:
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)
:
The negative of a C^nfunction 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)
:
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}
:
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)
:
The difference of two C^n functions is C^n.
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 (fun (x : E) => ∑ j ∈ u, f j x) s x = ∑ j ∈ u, iteratedFDerivWithin 𝕜 i (f j) s 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))
:
Product of two functions #
theorem
contDiff_mul
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{n : WithTop ℕ∞}
{𝔸 : Type u_3}
[NormedRing 𝔸]
[NormedAlgebra 𝕜 𝔸]
:
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)
:
The product of two C^nfunctions 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 : ℕ)
:
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 : 𝕜')
:
Scalar multiplication #
theorem
contDiff_smul
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{n : WithTop ℕ∞}
:
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 ℕ∞}
{s : Set E}
{f : E → 𝕜}
{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 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 ℕ∞}
{f : E → 𝕜}
{g : E → F}
(hf : ContDiffAt 𝕜 n f x)
(hg : ContDiffAt 𝕜 n g x)
:
ContDiffAt 𝕜 n (fun (x : E) => f x • g x) x
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 ℕ∞}
{f : E → 𝕜}
{g : E → F}
(hf : ContDiff 𝕜 n f)
(hg : ContDiff 𝕜 n g)
:
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 ℕ∞}
{s : Set E}
{f : E → 𝕜}
{g : E → F}
(hf : ContDiffOn 𝕜 n f s)
(hg : ContDiffOn 𝕜 n g s)
:
ContDiffOn 𝕜 n (fun (x : E) => f x • g x) s
The scalar multiplication of two C^n functions on a domain is C^n.
Constant scalar multiplication #
Porting note (https://github.com/leanprover-community/mathlib4/issues/11215): TODO: generalize results in this section.
- It should be possible to assume
[Monoid R] [DistribMulAction R F] [SMulCommClass 𝕜 R F]. - If
cis a unit (orRis a group), then one can dropContDiff*assumptions in some lemmas.
theorem
contDiff_const_smul
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{n : WithTop ℕ∞}
{R : Type u_3}
[Semiring R]
[Module R F]
[SMulCommClass 𝕜 R F]
[ContinuousConstSMul R F]
(c : R)
:
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}
[Semiring R]
[Module 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
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}
[Semiring R]
[Module 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
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}
[Semiring R]
[Module R F]
[SMulCommClass 𝕜 R F]
[ContinuousConstSMul R F]
{f : E → F}
(c : R)
(hf : ContDiff 𝕜 n f)
:
The scalar multiplication of a constant and a C^n function 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}
[Semiring R]
[Module 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 on a domain 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}
[Semiring R]
[Module R F]
[SMulCommClass 𝕜 R F]
[ContinuousConstSMul R F]
{i : ℕ}
{a : R}
(hf : ContDiffWithinAt 𝕜 (↑i) f s x)
(hu : UniqueDiffOn 𝕜 s)
(hx : x ∈ s)
:
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}
[Semiring R]
[Module R F]
[SMulCommClass 𝕜 R F]
[ContinuousConstSMul R F]
{i : ℕ}
{a : R}
(hf : ContDiffAt 𝕜 (↑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}
[Semiring R]
[Module R F]
[SMulCommClass 𝕜 R F]
[ContinuousConstSMul R F]
{i : ℕ}
{a : R}
(hf : ContDiffAt 𝕜 (↑i) f x)
:
Cartesian product of two functions #
theorem
ContDiffWithinAt.prod_map'
{𝕜 : 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.prod_map
{𝕜 : 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)
:
theorem
ContDiffOn.prod_map
{𝕜 : 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.prod_map
{𝕜 : 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.prod_map'
{𝕜 : 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.prod_map
{𝕜 : 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)
:
The product map of two C^n functions is C^n.
theorem
contDiff_prod_mk_left
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{n : WithTop ℕ∞}
(f₀ : F)
:
theorem
contDiff_prod_mk_right
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{n : WithTop ℕ∞}
(e₀ : E)
:
Inversion in a complete normed algebra (or more generally with summable geometric series) #
theorem
contDiffAt_ring_inverse
(𝕜 : 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 (fun (x : E) => (f x)⁻¹) s x
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 (fun (x : E) => (f x)⁻¹) s
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 (fun (x : E) => (f x)⁻¹) x
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)
:
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 (fun (x : E) => f x / g x) s x
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
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 (fun (x : E) => f x / g x) x
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)
:
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)
:
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
PartialHomeomorph.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 : PartialHomeomorph 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)
:
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
PartialHomeomorph.contDiffAt_symm_deriv
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{n : WithTop ℕ∞}
[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
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)
:
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
PartialHomeomorph.restrContDiff
(𝕜 : Type u_1)
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
(f : PartialHomeomorph E F)
(n : WithTop ℕ∞)
(hn : n ≠ ↑⊤)
:
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.
Equations
Instances For
@[simp]
theorem
PartialHomeomorph.restrContDiff_source
(𝕜 : Type u_1)
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
(f : PartialHomeomorph 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
PartialHomeomorph.restrContDiff_target
(𝕜 : Type u_1)
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
(f : PartialHomeomorph 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
PartialHomeomorph.restrContDiff_apply
(𝕜 : Type u_1)
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
(f : PartialHomeomorph E F)
(n : WithTop ℕ∞)
(hn : n ≠ ↑⊤)
(a✝ : E)
:
@[simp]
theorem
PartialHomeomorph.restrContDiff_symm_apply
(𝕜 : Type u_1)
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
(f : PartialHomeomorph E F)
(n : WithTop ℕ∞)
(hn : n ≠ ↑⊤)
(a✝ : F)
:
theorem
PartialHomeomorph.contDiffOn_restrContDiff_source
(𝕜 : Type u_1)
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
(f : PartialHomeomorph E F)
{n : WithTop ℕ∞}
(hn : n ≠ ↑⊤)
:
ContDiffOn 𝕜 n (↑f) (restrContDiff 𝕜 f n hn).source
theorem
PartialHomeomorph.contDiffOn_restrContDiff_target
(𝕜 : Type u_1)
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
(f : PartialHomeomorph 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