Hölder bounds from bounds on a function and its derivative

A function on a real normed space which is bounded by N₀, with derivative bounded by N₁, is α-Hölder for every α ≤ 1. By the mean value inequality it is N₁-Lipschitz on every convex set where the derivative bound holds, which is used between nearby points, and the bound N₀ controls its oscillation between distant points (HolderOnWith.of_le_of_dist_le).

Main declarations

• TauCeti.holderWith_of_norm_le_of_norm_fderiv_le: on the whole space, the Hölder constant is N₁ + 2 N₀.
• TauCeti.holderOnWith_thickening_of_norm_fderiv_le: if the bounds hold on an open set containing the 2δ-thickening of a set K, the function is Hölder on the δ-thickening of K.

theorem TauCeti.holderWith_of_norm_le_of_norm_fderiv_le {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {g : E → F} {N₀ N₁ α : NNReal} (hα : α ≤ 1) (hg : Differentiable ℝ g) (hg0 : ∀ (x : E), ‖g x‖ ≤ ↑N₀) (hg1 : ∀ (x : E), ‖fderiv ℝ g x‖ ≤ ↑N₁) : HolderWith (N₁ + 2 * N₀) α g

A differentiable function on the whole space bounded by N₀, with derivative bounded by N₁, is α-Hölder with constant N₁ + 2 N₀ for every α ≤ 1: it is N₁-Lipschitz, which is used at distances less than 1.

theorem TauCeti.holderOnWith_thickening_of_norm_fderiv_le {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω K : Set E} {g : E → F} {δ N₀ N₁ α : NNReal} (hδ : 0 < δ) (hα : α ≤ 1) (hΩ : IsOpen Ω) (hKΩ : Metric.thickening (2 * ↑δ) K ⊆ Ω) (hg : DifferentiableOn ℝ g Ω) (hg0 : ∀ x ∈ Ω, ‖g x‖ ≤ ↑N₀) (hg1 : ∀ x ∈ Ω, ‖fderiv ℝ g x‖ ≤ ↑N₁) : HolderOnWith (N₁ * δ ^ (1 - ↑α) + 2 * N₀ * δ ^ (-↑α)) α g (Metric.thickening (↑δ) K)

A function bounded by N₀, with derivative bounded by N₁, on an open set containing the 2δ-thickening of K is α-Hölder on the δ-thickening of K for every α ≤ 1, with constant N₁ δ^(1 - α) + 2 N₀ δ^(-α): nearby points of the δ-thickening lie in a ball of radius δ contained in the 2δ-thickening, on which the function is N₁-Lipschitz.