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
dist_le_integral_of_norm_deriv_le_of_le
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : ℝ → E}
{B : ℝ → ℝ}
{a 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)
:
theorem
dist_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)
: