Displacement is at most the integral of the speed

In this file we prove several version of the following fact: the displacement (dist (f a) (f b)) is at most the integral of ‖deriv f‖ over [a, b].

theorem norm_sub_le_integral_of_norm_deriv_le_of_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {a b : ℝ} {B : ℝ → ℝ} (hab : a ≤ b) (hfc : ContinuousOn f (Set.Icc a b)) (hfd : DifferentiableOn ℝ f (Set.Ioo a b)) (hfB : ∀ᵐ (t : ℝ), t ∈ Set.Ioo a b → ‖deriv f t‖ ≤ B t) (hBi : IntervalIntegrable B MeasureTheory.volume a b) : ‖f b - f a‖ ≤ ∫ (t : ℝ) in a..b, B t

Displacement is at most the integral of an upper estimate on the speed.

Let f : ℝ → E be a function which is continuous on a closed interval [a, b] and is differentiable on the open interval (a, b). If B t is an integrable upper estimate on ‖f' t‖, a < t < b, then ‖f b - f a‖ ≤ ∫ t in a..b, B t.

theorem norm_sub_le_mul_volume_of_norm_deriv_le_of_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {a b C : ℝ} (hab : a ≤ b) (hfc : ContinuousOn f (Set.Icc a b)) (hfd : DifferentiableOn ℝ f (Set.Ioo a b)) (hnorm : ∀ᵐ (t : ℝ), t ∈ Set.Ioo a b → ‖deriv f t‖ ≤ C) : ‖f b - f a‖ ≤ C * MeasureTheory.volume.real {x : ℝ | x ∈ Set.Ioo a b ∧ deriv f x ≠ 0}

Let f : ℝ → E be a function which is continuous on [a, b] and is differentiable on (a, b). Suppose that ‖f' t‖ ≤ C for a.e. t ∈ (a, b). Then the distance between f a and f b is at most C times the measure of x ∈ (a, b) such that f' x ≠ 0.

This lemma is useful, if f is known to have zero derivative at most points of [a, b].

theorem norm_sub_le_mul_volume_of_norm_lineDeriv_le {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E → F} {a b : E} {C : ℝ} (hfc : ContinuousOn f (segment ℝ a b)) (hfd : ∀ t ∈ Set.Ioo 0 1, LineDifferentiableAt ℝ f ((AffineMap.lineMap a b) t) (b - a)) (hf' : ∀ᵐ (t : ℝ), t ∈ Set.Ioo 0 1 → ‖lineDeriv ℝ f ((AffineMap.lineMap a b) t) (b - a)‖ ≤ C) : ‖f b - f a‖ ≤ C * MeasureTheory.volume.real {t : ℝ | t ∈ Set.Ioo 0 1 ∧ lineDeriv ℝ f ((AffineMap.lineMap a b) t) (b - a) ≠ 0}

Consider a function f : E → F continuous on a segment [a, b] and line differentiable in the direction b - a at all points of the open segment (a, b).

If ‖∂_{b - a} f‖ ≤ C at a.e. all points of the open segment, then ‖f b - f a‖ ≤ C * volume s, where s is the set of points t ∈ Ioo 0 1 such that f has nonzero line derivative in the direction b - a at lineMap a b t.

theorem norm_sub_le_mul_volume_of_norm_fderiv_le {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E → F} {a b : E} {C : ℝ} {s : Set E} (hs : IsOpen s) (hf : DiffContOnCl ℝ f s) (hab : openSegment ℝ a b ⊆ s) (hC : ∀ x ∈ s, ‖fderiv ℝ f x‖ ≤ C) : ‖f b - f a‖ ≤ C * ‖b - a‖ * MeasureTheory.volume.real {t : ℝ | t ∈ Set.Ioo 0 1 ∧ fderiv ℝ f ((AffineMap.lineMap a b) t) ≠ 0}

Let f : E → F be a function differentiable on a set s and continuous on its closure. Let a, b be two points such that the open segment connecting a to b is a subset of s.

If ‖Df‖ ≤ C everywhere on s then ‖f b - f a‖ ≤ C * volume u, where u is the set of points t ∈ Ioo 0 1 such that f has nonzero derivative at lineMap a b t.

theorem sub_isBigO_norm_rpow_add_one_of_fderiv {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E → F} {a : E} {r : ℝ} (hr : 0 ≤ r) (hdf : ∀ᶠ (x : E) in nhds a, DifferentiableAt ℝ f x) (hderiv : fderiv ℝ f =O[nhds a] fun (x : E) => ‖x - a‖ ^ r) : (fun (x : E) => f x - f a) =O[nhds a] fun (x : E) => ‖x - a‖ ^ (r + 1)

Let f : E → F be a function differentiable in a neighborhood of a. If $Df(x) = O(‖x - a‖ ^ r)$ as x → a, where r ≥ 0, then $f(x) - f(a) = O(‖x - a‖ ^ {r + 1})$ as x → a.

theorem isBigO_norm_rpow_add_one_of_fderiv_of_apply_eq_zero {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E → F} {a : E} {r : ℝ} (hr : 0 ≤ r) (hdf : ∀ᶠ (x : E) in nhds a, DifferentiableAt ℝ f x) (hderiv : fderiv ℝ f =O[nhds a] fun (x : E) => ‖x - a‖ ^ r) (hf₀ : f a = 0) : f =O[nhds a] fun (x : E) => ‖x - a‖ ^ (r + 1)

Let f : E → F be a function differentiable in a neighborhood of a. If $Df(x) = O(‖x - a‖ ^ r)$ as x → a, where r ≥ 0, and f a = 0, then $f(x) = O(‖x - a‖ ^ {r + 1})$ as x → a.