MATHLIBANNEX / CANONICAL DECLARATION CARD

A seminorm increment bound passes to every derivative direction

MathlibAnnex.FDeriv.norm_apply_le_seminorm_of_lipschitz

theorem

Takes a difference-quotient limit without imposing a positive lower bound.

Statement

Let , let and have the sup norms, and let be a real seminorm. Let satisfy Fix a point at which is Fréchet differentiable, and write for its derivative. Then

Assumptions

The seminorm may be degenerate. Neither norm equivalence nor a positive lower comparison is assumed. The increment estimate holds globally; differentiability is assumed only at the chosen point. Both dimensions may be zero.

Conclusion

The same seminorm bounds for every direction, including zero.

Let denote coordinate Lebesgue measure on . The separate almost-everywhere wrapper additionally takes with . Then , so Rademacher gives differentiability almost everywhere for reference Lebesgue measure. Restriction to any set and the pointwise result give the bound for every , for -almost every . The extra upper comparison is an input of this wrapper.

Proof route

Apply the increment estimate on one affine line, then pass to its derivative.

Proof steps

  1. Estimate one directional quotient. Fix and let . The increment assumption and seminorm homogeneity give

    For every real , division by gives

    This also applies to .

  2. Take the derivative limit. Differentiability at gives

    Continuity of the norm therefore yields

    The source’s local derivative-bound argument uses , and . The previous estimate and this derivative limit are its inputs; its output is exactly the asserted inequality.

Main citations

Lean source signature (exact)

/-- A seminorm increment bound passes to the derivative in each direction. -/
theorem norm_apply_le_seminorm_of_lipschitz {n N : ℕ}
    (p : Seminorm ℝ (Fin n → ℝ)) {f : (Fin n → ℝ) → (Fin N → ℝ)}
    (hf : ∀ x y, ‖f x - f y‖ ≤ p (x - y)) {x : Fin n → ℝ}
    (hx : DifferentiableAt ℝ f x) : ∀ v, ‖(fderiv ℝ f x) v‖ ≤ p v

Read hf and hx as the two hypotheses; neither is an additional map.

In the source Mathematical meaning
{n N : ℕ} Arbitrary nonnegative integers . Braces mean that Lean may infer these parameters; they are not extra assumptions.
Fin n → ℝ; Fin N → ℝ The spaces and with their sup norms. A vector is a list of real coordinates, indexed from in Lean and from in the formulas here.
p : Seminorm ℝ (Fin n → ℝ) A real seminorm : , and . It may vanish at a nonzero vector.
{f : ... → ...}; {x : Fin n → ℝ} The function and the chosen point . Braces let Lean infer these inputs.
hf : ∀ x y, ‖f x - f y‖ ≤ p (x - y) The global hypothesis for every . The bound variables called here range independently of the later chosen point .
hx : DifferentiableAt ℝ f x The function is Fréchet differentiable over at the chosen point .
In the source Mathematical meaning
(fderiv ℝ f x) v Apply the linear derivative to the direction ; this is the vector , not a scalar derivative.
∀ v, ‖(fderiv ℝ f x) v‖ ≤ p v The conclusion for every . There is no almost-everywhere qualifier or measure in this theorem.
Exact surrounding binder context (separate excerpts)

Exact source lines 17–22:

noncomputable section

open Set MeasureTheory Filter
open scoped Topology

namespace MathlibAnnex.FDeriv

Read exact source with highlighted declaration · Raw UTF-8 source · Card PDF · Back to Project

Exact content identity

Declaration: MathlibAnnex.FDeriv.norm_apply_le_seminorm_of_lipschitz

Accepted content SHA-256: 5b41411f5dc056e27160fcebab5aa5e88e29a47ac8906cf19dabab8f075a2596

Accepted source guide SHA-256: 0ee2158dfd51abb0dd4d0afc25dfcffcfada4614c2964db213f54bb54f75f398

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Back to top ↑