The increment of a function along a segment

This file bounds the increment of a function between x and x + h by the integral of its directional derivative along the segment joining them. It is the multi-dimensional form of Mathlib's one-dimensional enorm_sub_le_lintegral_deriv_of_contDiffOn_Icc, obtained by composing with the affine parametrization t ↦ x + t • h of the segment.

The hypotheses of the first estimate are local to the segment: differentiability at each of its points and continuity of the directional derivative along it. The normalized real-valued estimate instead assumes continuity of the function along the parameterized segment, differentiability at interior parameters, and interval integrability of the norm of the full Fréchet derivative rather than continuity merely of its fixed directional evaluation; these hypotheses are needed only when the segment has positive length.

Main declarations

• TauCeti.enorm_sub_le_lintegral_enorm_fderiv_apply: the segment increment estimate.
• TauCeti.norm_sub_le_integral_norm_fderiv_along_segment: the corresponding normalized real-integral estimate.

References

L. C. Evans, Partial Differential Equations, Chapter 5, where this is the starting point of the difference-quotient characterization of Sobolev functions.

theorem TauCeti.enorm_sub_le_lintegral_enorm_fderiv_apply {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {u : E → F} (x h : E) (hd : ∀ t ∈ Set.Icc 0 1, DifferentiableAt ℝ u (x + t • h)) (hc : ContinuousOn (fun (t : ℝ) => (fderiv ℝ u (x + t • h)) h) (Set.Icc 0 1)) : ‖u (x + h) - u x‖ₑ ≤ ∫⁻ (t : ℝ) in Set.Icc 0 1, ‖(fderiv ℝ u (x + t • h)) h‖ₑ

The segment increment estimate: the norm of u (x + h) - u x is at most the integral along the segment from x to x + h of the norm of the directional derivative Du(x + t • h) h.

theorem TauCeti.norm_sub_le_integral_norm_fderiv_along_segment {E : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {u : E → F} (x y : E) (h : x = y ∨ x ≠ y ∧ (∀ t ∈ Set.Ioo 0 ‖x - y‖, DifferentiableAt ℝ u (x + t • ‖x - y‖⁻¹ • (y - x))) ∧ ContinuousOn (fun (t : ℝ) => u (x + t • ‖x - y‖⁻¹ • (y - x))) (Set.Icc 0 ‖x - y‖) ∧ IntervalIntegrable (fun (t : ℝ) => ‖fderiv ℝ u (x + t • ‖x - y‖⁻¹ • (y - x))‖) MeasureTheory.volume 0 ‖x - y‖) : ‖u x - u y‖ ≤ ∫ (t : ℝ) in 0..‖x - y‖, ‖fderiv ℝ u (x + t • ‖x - y‖⁻¹ • (y - x))‖

The oscillation of a function along a segment is bounded by the integrated norm of its Fréchet derivative along that segment. For distinct endpoints, the function is continuous along the closed parameter interval, differentiable at its interior parameters, and the operator-norm bound is interval-integrable. The zero-length segment requires no analytic hypotheses.

This is adapted from Scott Armstrong and Julia Kempe's Apache-2.0 scottnarmstrong/DeGiorgi/DeGiorgi/Poincare.lean, commit 4c1b3077d3782b24065184df4ba59501b2e56fc7, lines 382--431.