Continuously k times differentiable functions with pointwise Hölder continuous derivatives #
We say that a function is of class $C^{k+(α)}$ at a point a,
where k is a natural number and 0 ≤ α ≤ 1, if
- it is of class $C^k$ at
ain the sense ofContDiffAt; - its
kth derivative satisfies $D^kf(x)-D^kf(a) = O(‖x - a‖ ^ α)$ asx → a.
Note that the Hölder condition used in this definition fixes one of the points at a.
In different sources, it is called pointwise, local, or weak Hölder condition,
though the term "local" may also mean a stronger condition
saying that a function is Hölder continuous on a neighborhood of a.
The immediate reason for adding this definition to the library is its use in [Mor01], where Moreira proves a version of the Morse-Sard theorem for functions that satisfy this condition on their critical set.
In this file, we define ContDiffPointwiseHolderAt to be the predicate
saying that a function is $C^{k+(α)}$ in the sense described above
and prove basic properties of this predicate.
Implementation notes #
In Moreira's paper, k is assumed to be a strictly positive number.
We define the predicate for any k : ℕ, then assume k ≠ 0 whenever it is necessary.
structure
ContDiffPointwiseHolderAt
{E : Type u_1}
{F : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
(k : ℕ)
(α : ↑unitInterval)
(f : E → F)
(a : E)
:
A map f is said to be $C^{k+(α)}$ at a, where k is a natural number and 0 ≤ α ≤ 1,
if it is $C^k$ at this point and $D^kf(x)-D^kf(a) = O(‖x - a‖ ^ α)$ as x → a.
When naming lemmas about this predicate, k is called "order", and α is called "exponent".
- contDiffAt : ContDiffAt ℝ (↑k) f a
A $C^{k+(α)}$ map is a $C^k$ map.
- isBigO : (fun (x : E) => iteratedFDeriv ℝ k f x - iteratedFDeriv ℝ k f a) =O[nhds a] fun (x : E) => ‖x - a‖ ^ ↑α
A $C^{k+(α)}$ map satisfies $D^kf(x)-D^kf(a) = O(‖x - a‖ ^ α)$ as
x → a.
Instances For
theorem
contDiffPointwiseHolderAt_iff
{E : Type u_1}
{F : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
(k : ℕ)
(α : ↑unitInterval)
(f : E → F)
(a : E)
:
ContDiffPointwiseHolderAt k α f a ↔ ContDiffAt ℝ (↑k) f a ∧ (fun (x : E) => iteratedFDeriv ℝ k f x - iteratedFDeriv ℝ k f a) =O[nhds a] fun (x : E) => ‖x - a‖ ^ ↑α
theorem
ContDiffAt.contDiffPointwiseHolderAt
{E : Type u_1}
{F : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{k : ℕ}
{f : E → F}
{a : E}
{n : WithTop ℕ∞}
(h : ContDiffAt ℝ n f a)
(hk : ↑k < n)
(α : ↑unitInterval)
:
ContDiffPointwiseHolderAt k α f a
A $C^n$ map is a $C^{k+(α)}$ map for any k < n.
theorem
ContDiffPointwiseHolderAt.continuousAt
{E : Type u_1}
{F : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{k : ℕ}
{α : ↑unitInterval}
{f : E → F}
{a : E}
(h : ContDiffPointwiseHolderAt k α f a)
:
ContinuousAt f a
theorem
ContDiffPointwiseHolderAt.differentiableAt
{E : Type u_1}
{F : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{k : ℕ}
{α : ↑unitInterval}
{f : E → F}
{a : E}
(h : ContDiffPointwiseHolderAt k α f a)
(hk : k ≠ 0)
:
DifferentiableAt ℝ f a
@[simp]
theorem
ContDiffPointwiseHolderAt.zero_exponent_iff
{E : Type u_1}
{F : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{k : ℕ}
{f : E → F}
{a : E}
:
A function is $C^{k+(0)}$ at a point if and only if it is $C^k$ at the point.
theorem
ContDiffPointwiseHolderAt.zero_order_iff
{E : Type u_1}
{F : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{α : ↑unitInterval}
{f : E → F}
{a : E}
:
A function is $C^{0+(α)}$ at a point if and only if it is $C^0$ at the point (i.e., it is continuous on a neighborhood of the point) and $f(x) - f(a) = O(‖x - a‖ ^ α)$.
theorem
ContDiffPointwiseHolderAt.of_exponent_le
{E : Type u_1}
{F : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{k : ℕ}
{α β : ↑unitInterval}
{f : E → F}
{a : E}
(hf : ContDiffPointwiseHolderAt k α f a)
(hle : β ≤ α)
:
ContDiffPointwiseHolderAt k β f a
theorem
ContDiffPointwiseHolderAt.of_order_lt
{E : Type u_1}
{F : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{k l : ℕ}
{α β : ↑unitInterval}
{f : E → F}
{a : E}
(hf : ContDiffPointwiseHolderAt k α f a)
(hlt : l < k)
:
ContDiffPointwiseHolderAt l β f a
theorem
ContDiffPointwiseHolderAt.of_toLex_le
{E : Type u_1}
{F : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{k l : ℕ}
{α β : ↑unitInterval}
{f : E → F}
{a : E}
(hf : ContDiffPointwiseHolderAt k α f a)
(hle : toLex (l, β) ≤ toLex (k, α))
:
ContDiffPointwiseHolderAt l β f a
theorem
ContDiffPointwiseHolderAt.of_order_le
{E : Type u_1}
{F : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{k l : ℕ}
{α : ↑unitInterval}
{f : E → F}
{a : E}
(hf : ContDiffPointwiseHolderAt k α f a)
(hl : l ≤ k)
:
ContDiffPointwiseHolderAt l α f a
theorem
ContDiffPointwiseHolderAt.of_contDiffOn_holderOnWith
{E : Type u_1}
{F : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{k : ℕ}
{α : ↑unitInterval}
{f : E → F}
{a : E}
{s : Set E}
{C : NNReal}
(hf : ContDiffOn ℝ (↑k) f s)
(hs : s ∈ nhds a)
(hd : HolderOnWith C ⟨↑α, ⋯⟩ (iteratedFDeriv ℝ k f) s)
:
ContDiffPointwiseHolderAt k α f a
If a function is $C^{k+α}$ on a neighborhood of a point a,
i.e., it is $C^k$ on this neighborhood and $D^k f$ is Hölder continuous on it,
then the function is $C^{k+(α)}$ at a.
theorem
ContDiffPointwiseHolderAt.fst
{E : Type u_1}
{F : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{k : ℕ}
{α : ↑unitInterval}
{a : E × F}
:
theorem
ContDiffPointwiseHolderAt.snd
{E : Type u_1}
{F : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{k : ℕ}
{α : ↑unitInterval}
{a : E × F}
:
theorem
ContDiffPointwiseHolderAt.prodMk
{E : Type u_1}
{F : Type u_2}
{G : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[NormedAddCommGroup G]
[NormedSpace ℝ G]
{k : ℕ}
{α : ↑unitInterval}
{f : E → F}
{a : E}
{g : E → G}
(hf : ContDiffPointwiseHolderAt k α f a)
(hg : ContDiffPointwiseHolderAt k α g a)
:
ContDiffPointwiseHolderAt k α (fun (x : E) => (f x, g x)) a
theorem
ContDiffPointwiseHolderAt.comp_of_differentiableAt
{E : Type u_1}
{F : Type u_2}
{G : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[NormedAddCommGroup G]
[NormedSpace ℝ G]
{k : ℕ}
{α : ↑unitInterval}
{f : E → F}
(a : E)
{g : F → G}
(hg : ContDiffPointwiseHolderAt k α g (f a))
(hf : ContDiffPointwiseHolderAt k α f a)
(hd : DifferentiableAt ℝ g (f a) ∨ DifferentiableAt ℝ f a)
:
ContDiffPointwiseHolderAt k α (g ∘ f) a
Composition of two $C^{k+(α)}$ functions is a $C^{k+(α)}$ function, provided that one of them is differentiable.
The latter condition follows automatically from the functions being $C^{k+(α)}$,
if k ≠ 0, see comp below.
theorem
ContDiffPointwiseHolderAt.comp
{E : Type u_1}
{F : Type u_2}
{G : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[NormedAddCommGroup G]
[NormedSpace ℝ G]
{k : ℕ}
{α : ↑unitInterval}
{f : E → F}
(a : E)
{g : F → G}
(hg : ContDiffPointwiseHolderAt k α g (f a))
(hf : ContDiffPointwiseHolderAt k α f a)
(hk : k ≠ 0)
:
ContDiffPointwiseHolderAt k α (g ∘ f) a
Composition of two $C^{k+(α)}$ functions, k ≠ 0, is a $C^{k+(α)}$ function.
theorem
ContDiffPointwiseHolderAt.comp₂_of_differentiableAt
{E : Type u_1}
{F : Type u_2}
{G : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[NormedAddCommGroup G]
[NormedSpace ℝ G]
{k : ℕ}
{α : ↑unitInterval}
(a : E)
{H : Type u_4}
[NormedAddCommGroup H]
[NormedSpace ℝ H]
{g : F × G → H}
{f₁ : E → F}
{f₂ : E → G}
(hg : ContDiffPointwiseHolderAt k α g (f₁ a, f₂ a))
(hf₁ : ContDiffPointwiseHolderAt k α f₁ a)
(hf₂ : ContDiffPointwiseHolderAt k α f₂ a)
(hdiff : DifferentiableAt ℝ g (f₁ a, f₂ a) ∨ DifferentiableAt ℝ f₁ a ∧ DifferentiableAt ℝ f₂ a)
:
ContDiffPointwiseHolderAt k α (fun (x : E) => g (f₁ x, f₂ x)) a
theorem
ContinuousLinearMap.contDiffPointwiseHolderAt
{E : Type u_1}
{F : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{k : ℕ}
{α : ↑unitInterval}
{a : E}
(f : E →L[ℝ] F)
:
ContDiffPointwiseHolderAt k α (⇑f) a
theorem
ContinuousLinearEquiv.contDiffPointwiseHolderAt
{E : Type u_1}
{F : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{k : ℕ}
{α : ↑unitInterval}
{a : E}
(f : E ≃L[ℝ] F)
:
ContDiffPointwiseHolderAt k α (⇑f) a
theorem
ContDiffPointwiseHolderAt.continuousLinearMap_comp
{E : Type u_1}
{F : Type u_2}
{G : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[NormedAddCommGroup G]
[NormedSpace ℝ G]
{k : ℕ}
{α : ↑unitInterval}
{f : E → F}
{a : E}
(hf : ContDiffPointwiseHolderAt k α f a)
(g : F →L[ℝ] G)
:
ContDiffPointwiseHolderAt k α (⇑g ∘ f) a
@[simp]
theorem
ContinuousLinearEquiv.contDiffPointwiseHolderAt_left_comp
{E : Type u_1}
{F : Type u_2}
{G : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[NormedAddCommGroup G]
[NormedSpace ℝ G]
{k : ℕ}
{α : ↑unitInterval}
{f : E → F}
{a : E}
(g : F ≃L[ℝ] G)
:
@[simp]
theorem
LinearIsometryEquiv.contDiffPointwiseHolderAt_left_comp
{E : Type u_1}
{F : Type u_2}
{G : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[NormedAddCommGroup G]
[NormedSpace ℝ G]
{k : ℕ}
{α : ↑unitInterval}
{f : E → F}
{a : E}
(g : F ≃ₗᵢ[ℝ] G)
:
theorem
ContDiffPointwiseHolderAt.id
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{k : ℕ}
{α : ↑unitInterval}
{a : E}
:
ContDiffPointwiseHolderAt k α id a
theorem
ContDiffPointwiseHolderAt.const
{E : Type u_1}
{F : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{k : ℕ}
{α : ↑unitInterval}
{a : E}
{b : F}
:
ContDiffPointwiseHolderAt k α (Function.const E b) a
theorem
ContDiffPointwiseHolderAt.fderiv
{E : Type u_1}
{F : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{k l : ℕ}
{α : ↑unitInterval}
{f : E → F}
{a : E}
(hf : ContDiffPointwiseHolderAt k α f a)
(hl : l < k)
:
ContDiffPointwiseHolderAt l α (fderiv ℝ f) a
The derivative of a $C^{k + (α)}$ function is a $C^{l + (α)}$ function, if l < k.
theorem
ContDiffPointwiseHolderAt.iteratedFDeriv
{E : Type u_1}
{F : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{k l m : ℕ}
{α : ↑unitInterval}
{f : E → F}
{a : E}
(hf : ContDiffPointwiseHolderAt k α f a)
(hl : l + m ≤ k)
:
ContDiffPointwiseHolderAt l α (iteratedFDeriv ℝ m f) a
If f is a $C^{k+(α)}$ function and l + m ≤ k, then $D^mf$ is a $C^{l + (α)}$ function.
theorem
ContDiffPointwiseHolderAt.congr_of_eventuallyEq
{E : Type u_1}
{F : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{k : ℕ}
{α : ↑unitInterval}
{f : E → F}
{a : E}
{g : E → F}
(hf : ContDiffPointwiseHolderAt k α f a)
(hfg : f =ᶠ[nhds a] g)
:
ContDiffPointwiseHolderAt k α g a
theorem
ContDiffPointwiseHolderAt.clm_apply
{E : Type u_1}
{F : Type u_2}
{G : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[NormedAddCommGroup G]
[NormedSpace ℝ G]
{k : ℕ}
{α : ↑unitInterval}
{a : E}
{f : E → F →L[ℝ] G}
{g : E → F}
(hf : ContDiffPointwiseHolderAt k α f a)
(hg : ContDiffPointwiseHolderAt k α g a)
:
ContDiffPointwiseHolderAt k α (fun (x : E) => (f x) (g x)) a