Mean value estimates

A directional mean value inequality

The mean value inequality only needs control of the derivative in the direction of the chord being estimated, not an operator norm bound. This is useful on lower-dimensional simplices, where derivatives are determined only on tangent directions, and when estimating a parametrized map in terms of the size of its geometric chord.

The argument follows Mathlib's Convex.norm_image_sub_le_of_norm_hasFDerivWithin_le, using its one-variable mean value inequality along the same line segment.

Escaping a superlevel set at bounded speed

Let w be a differentiable real function on a real normed space whose derivative has norm at most L on the band {a ≤ w ≤ b}. Starting from a point where w ≥ b, the function cannot reach the level a within distance (b - a) / L (TauCeti.lt_apply_add_of_norm_fderiv_le). Consequently the outer shell of the r-thickening of {w ≥ 0} lies in {-(L r) < w < 0} when ‖Dw‖ ≤ L on {-(L r) ≤ w ≤ 0} (Differentiable.thickening_sdiff_subset_preimage_Ioo_of_norm_fderiv_le).

Mathlib's Convex.norm_image_sub_le_of_norm_fderiv_le needs the derivative bound along the whole segment; here it is only assumed on the band, which is what is available near a level set of a function whose gradient is controlled only there. The proof applies the one-variable mean value theorem on the part of the segment where the function crosses the band.

The file also records the one-variable form of Mathlib's Convex.norm_image_sub_le_of_norm_hasFDerivWithin_le', bounding the increment of a function against a fixed derivative φ (Convex.norm_image_sub_le_of_norm_hasDerivWithin_le').

For a function on the real line with derivative of norm at most D r ^ (β - 1) at every r > 0, where 0 ≤ β ≤ 1, the increments satisfy ‖u b - u a‖ ≤ 2 D |b - a| a ^ (β - 1) for a > 0 and a / 2 ≤ b (TauCeti.norm_sub_le_mul_abs_sub_mul_rpow_of_hasDerivAt).

Space-time functions vanishing outside a time interval

A function of time and space with derivative bounded by C that vanishes outside the time interval (a, b) is bounded by C (b - a), by the mean value inequality from its value at the time a (TauCeti.norm_le_mul_sub_of_forall_notMem_Ioo_eq_zero).

Comparing maps with nearby derivatives

If two maps on a convex set have derivatives within ε of a common linear map and agree at a point y, then by the mean value inequality applied to their difference they stay within 2 ε ‖x - y‖ of each other (Convex.norm_sub_le_of_norm_hasFDerivWithin_sub_le). This compares a map to a model agreeing with it to first order before splicing them together (TauCeti.Analysis.Calculus.Splice).

For an antilipschitz parametrization with bounded derivative, an image chord controls the parametric chord and its intervening points. A scalar mean value estimate permits bounds on individual coordinate derivatives. These estimates are adapted from KLS, commit 65810c73f9dd7945fc646ab484cb19d673f5291d, formalization/FunctionalInequalities/Analysis/Sard/Disk.lean.

Invariance along a direction

Over ℝ or ℂ, a map whose derivative kills a vector v at every point z + t • v of the segment from z to z + v (t real, 0 ≤ t ≤ 1) takes the same value at z and z + v (TauCeti.apply_add_eq_of_fderiv_apply_eq_zero). Unlike Mathlib's Convex.is_const_of_fderivWithin_eq_zero, only the derivative in the direction v is assumed to vanish, so the map need not be constant near the segment. Consequently, if π is a continuous projection and the derivative of a map kills ker π on a ball about 0, then near 0 the map only depends on the π component (TauCeti.apply_proj_eq_of_fderiv_apply_eq_zero).

theorem Convex.norm_sub_le_of_norm_hasFDerivWithin_sub_le {X : Type u_1} {Y : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] {S : Set X} (hS : Convex ℝ S) {k l : X → Y} {k' l' : X → X →L[ℝ] Y} {A : X →L[ℝ] Y} {ε : ℝ} (hk : ∀ x ∈ S, HasFDerivWithinAt k (k' x) S x) (hl : ∀ x ∈ S, HasFDerivWithinAt l (l' x) S x) (hk' : ∀ x ∈ S, ‖k' x - A‖ ≤ ε) (hl' : ∀ x ∈ S, ‖l' x - A‖ ≤ ε) {x y : X} (hx : x ∈ S) (hy : y ∈ S) (hxy : k y = l y) : ‖l x - k x‖ ≤ 2 * ε * ‖x - y‖

Two maps with nearby derivatives that agree at a point stay close. If the derivatives of k and l on a convex set S are within ε of a fixed linear map A, and k and l agree at y ∈ S, then ‖l x - k x‖ ≤ 2 ε ‖x - y‖ for every x ∈ S.

theorem Convex.norm_image_sub_le_of_norm_hasFDerivWithin_apply_le {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} {f : E → F} {f' : E → E →L[𝕜] F} {x y : E} {C : ℝ} (hs : Convex ℝ s) (hf : ∀ z ∈ s, HasFDerivWithinAt f (f' z) s z) (hbound : ∀ z ∈ segment ℝ x y, ‖(f' z) (y - x)‖ ≤ C) (hx : x ∈ s) (hy : y ∈ s) : ‖f y - f x‖ ≤ C

The mean value inequality with a bound only in the direction of the chord. The bound is needed only on the segment joining the endpoints. In particular, neither an operator norm bound nor a full-dimensional domain is required. Derivatives may be taken over a real or complex scalar field.

theorem TauCeti.lt_apply_add_of_norm_fderiv_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {w : E → ℝ} (hw : Differentiable ℝ w) {a b L : ℝ} (hL : 0 ≤ L) (hbound : ∀ (x : E), a ≤ w x → w x ≤ b → ‖fderiv ℝ w x‖ ≤ L) {x z : E} (hx : b ≤ w x) (hz : L * ‖z‖ < b - a) : a < w (x + z)

If the derivative of w has norm at most L wherever a ≤ w ≤ b, then w stays above a at distance less than (b - a) / L from every point where w ≥ b.

theorem TauCeti.norm_sub_le_of_norm_fderiv_sub_id_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {c : E} {h : E → E} {r δ : ℝ} (hhc : h c = c) (hhd : ∀ x ∈ Metric.closedBall c (2 * r), HasFDerivAt (fun (y : E) => h y - y) (fderiv ℝ h x - ContinuousLinearMap.id ℝ E) x) (hδ : ∀ x ∈ Metric.closedBall c (2 * r), ‖fderiv ℝ h x - ContinuousLinearMap.id ℝ E‖ ≤ δ) {x : E} (hx : x ∈ Metric.closedBall c (2 * r)) : ‖h x - x‖ ≤ δ * (2 * r)

The mean value inequality: if h fixes c and h - id has derivative of norm at most δ on the closed ball of radius 2 r about c, then h - id moves points of this ball by at most δ * (2 * r).

theorem TauCeti.norm_sub_le_mul_abs_sub_mul_rpow_of_hasDerivAt {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {u f' : ℝ → F} {β D : ℝ} (hβ₀ : 0 ≤ β) (hβ₁ : β - 1 ≤ 0) (hderiv : ∀ (r : ℝ), 0 < r → HasDerivAt u (f' r) r) (hbound : ∀ (r : ℝ), 0 < r → ‖f' r‖ ≤ D * r ^ (β - 1)) {a b : ℝ} (ha : 0 < a) (hb : a / 2 ≤ b) : ‖u b - u a‖ ≤ 2 * D * (|b - a| * a ^ (β - 1))

Mean value bound near a > 0: if u has derivative f' r of norm at most D r^(β - 1) at every r > 0 (0 ≤ β ≤ 1), then ‖u b - u a‖ ≤ 2 D |b - a| a^(β - 1) for a / 2 ≤ b.

theorem TauCeti.apply_add_eq_of_fderiv_apply_eq_zero {𝕂 : Type u_2} [RCLike 𝕂] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕂 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕂 G] {g : F → G} {z v : F} (hg : ∀ t ∈ Set.Icc 0 1, DifferentiableAt 𝕂 g (z + ↑t • v)) (hv : ∀ t ∈ Set.Icc 0 1, (fderiv 𝕂 g (z + ↑t • v)) v = 0) : g (z + v) = g z

If g is differentiable at every point z + t • v of the segment from z to z + v, for real 0 ≤ t ≤ 1, and its derivative kills v there, then g takes the same value at z and at z + v.

theorem TauCeti.apply_proj_eq_of_fderiv_apply_eq_zero {𝕂 : Type u_2} [RCLike 𝕂] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕂 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕂 G] {g : F → G} {π : F →L[𝕂] F} (hπ : IsIdempotentElem π) {r : ℝ} (hg : DifferentiableOn 𝕂 g (Metric.ball 0 r)) (hker : ∀ u ∈ Metric.ball 0 r, ∀ (v : F), π v = 0 → (fderiv 𝕂 g u) v = 0) {z : F} (hz : ‖π z‖ + ‖z - π z‖ < r) : g (π z) = g z

Let π be a continuous projection of F. If g is differentiable on the ball of radius r about 0 and its derivative there kills the kernel of π, then g only depends on the π component on the part of that ball where ‖π z‖ + ‖z - π z‖ < r.

theorem TauCeti.norm_le_mul_sub_of_forall_notMem_Ioo_eq_zero {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} {φ : ℝ × E → ℝ} (hφd : Differentiable ℝ φ) {C : ℝ} (hC : ∀ (q : ℝ × E), ‖fderiv ℝ φ q‖ ≤ C) (hzero : ∀ (q : ℝ × E), q.1 ∉ Set.Ioo a b → φ q = 0) (hab : a ≤ b) (q : ℝ × E) : ‖φ q‖ ≤ C * (b - a)

A function with derivative bounded by C that vanishes outside the time interval (a, b) is bounded by C * (b - a), by the mean value inequality from its value at the time a.

theorem Differentiable.thickening_sdiff_subset_preimage_Ioo_of_norm_fderiv_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {w : E → ℝ} (hw : Differentiable ℝ w) {L r : ℝ} (hL : 0 < L) (hgrad : ∀ (x : E), -(L * r) ≤ w x → w x ≤ 0 → ‖fderiv ℝ w x‖ ≤ L) : Metric.thickening r {x : E | 0 ≤ w x} \ {x : E | 0 ≤ w x} ⊆ w ⁻¹' Set.Ioo (-(L * r)) 0

The outer shell of a thickening of a superlevel set lies in a level band. Let w be differentiable with ‖Dw‖ ≤ L wherever -(L r) ≤ w ≤ 0. Then the part of the open r-neighbourhood of {w ≥ 0} outside {w ≥ 0} lies in {-(L r) < w < 0}.

theorem Convex.norm_image_sub_le_of_norm_hasDerivWithin_le' {𝕜 : Type u_1} {G : Type u_2} [RCLike 𝕜] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f f' : 𝕜 → G} {s : Set 𝕜} {x y : 𝕜} {φ : G} {C : ℝ} (hf : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x) (bound : ∀ x ∈ s, ‖f' x - φ‖ ≤ C) (hs : Convex ℝ s) (xs : x ∈ s) (ys : y ∈ s) : ‖f y - f x - (y - x) • φ‖ ≤ C * ‖y - x‖

Variant of the mean value inequality on a convex set in dimension 1, using a bound on the difference between the derivative and a fixed vector φ, rather than a bound on the derivative itself. Version with HasDerivWithinAt.

theorem Differentiable.norm_sub_le_mul_of_segment {P : Type u_1} {Q : Type u_2} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup Q] [NormedSpace ℝ Q] {φ : P → Q} (hφd : Differentiable ℝ φ) {C κ : ℝ} (hbound : ∀ x ∈ Metric.closedBall 0 1, ‖fderiv ℝ φ x‖ ≤ C) (hanti : ∀ a ∈ Metric.closedBall 0 1, ∀ b ∈ Metric.closedBall 0 1, ‖a - b‖ ≤ κ * ‖φ a - φ b‖) {a b : P} (ha : a ∈ Metric.closedBall 0 1) (hb : b ∈ Metric.closedBall 0 1) {s t : ℝ} (hs : s ∈ Set.Icc 0 1) (ht : t ∈ Set.Icc 0 s) : ‖φ a - φ (a + t • (b - a))‖ ≤ C * κ * ‖φ a - φ (a + s • (b - a))‖

A chord in a closed unit ball remains uniformly close in the image to its initial point, relative to the image distance to a prescribed intermediate point, if the parametrization has bounded derivative and is antilipschitz on the ball.

theorem Differentiable.abs_sub_le_of_basis_bound {P : Type u_1} [NormedAddCommGroup P] [NormedSpace ℝ P] {n : ℕ} {φ : P → Fin n → ℝ} (hφd : Differentiable ℝ φ) {f : (Fin n → ℝ) → ℝ} (hf : Differentiable ℝ f) {C D : ℝ} (hD : 0 ≤ D) (hbound : ∀ x ∈ Metric.closedBall 0 1, ‖fderiv ℝ φ x‖ ≤ C) {a b : P} (ha : a ∈ Metric.closedBall 0 1) (hb : b ∈ Metric.closedBall 0 1) {s : ℝ} (hs : s ∈ Set.Icc 0 1) (hcoord : ∀ t ∈ Set.Ico 0 s, ∀ (j : Fin n), |(fderiv ℝ f (φ (a + t • (b - a)))) (Pi.single j 1)| ≤ D) : |f (φ (a + s • (b - a))) - f (φ a)| ≤ ↑n * (C * ‖b - a‖) * D * s

The mean value estimate along a parametrized chord, with bounds on the coordinate derivatives of a real-valued function and the derivative of the parametrization.

theorem ContDiff.exists_norm_sub_le_mul_max_uncurry {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {Γ : ℝ → ℝ → E} (hΓ : ContDiff ℝ 1 (Function.uncurry Γ)) (t₀ t₀' a b : ℝ) : ∃ (B : NNReal), ∀ ⦃x₁ y₁ x₂ y₂ : ℝ⦄, x₁ ∈ Set.Icc t₀ t₀' → y₁ ∈ Set.Icc a b → x₂ ∈ Set.Icc t₀ t₀' → y₂ ∈ Set.Icc a b → ‖Γ x₁ y₁ - Γ x₂ y₂‖ ≤ ↑B * max |x₁ - x₂| |y₁ - y₂|

Lipschitz bound for a jointly C¹ family on a box. If Γ t s is C¹ in (t, s), there is a constant B such that ‖Γ t₁ s₁ - Γ t₂ s₂‖ ≤ B * max |t₁ - t₂| |s₁ - s₂| for all t₁, t₂ in [t₀, t₁'] and all s₁, s₂ in [a, b].

theorem IsPreconnected.eq_of_hasDerivWithinAt_zero {G : Type u_1} [NormedAddCommGroup G] [NormedSpace ℝ G] {f : ℝ → G} {s : Set ℝ} (hs : IsPreconnected s) (hf : ∀ t ∈ s, HasDerivWithinAt f 0 s t) {a b : ℝ} (ha : a ∈ s) (hb : b ∈ s) : f a = f b

A function on a preconnected subset of ℝ whose derivative within the set vanishes at every point of the set takes the same value at any two points of the set.