Samplinglib mathematical lesson

A totalized derivative bound for the scaled norm

AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Cutoff.fderiv_norm_div_bound · theorem · Teaching coverage

Read this first

Mathematical statement

Let E be a real normed vector space and R>0. At every x∈E, the operator norm of Mathlib's totalized Fréchet derivative of y↦‖y‖/R is at most 1/R. No differentiability assumption on the norm at x is made.

\[R>0\quad\Longrightarrow\quad\forall x\in E,\quad\left\|D_{\mathrm{tot}}\!\left(y\mapsto\frac{\|y\|}{R}\right)(x)\right\|_{\mathrm{op}}\le\frac1R.\]

Lean statement · fderiv_norm_div_bound

`[NormedSpace ℝ E]` is required to speak about a real Fréchet derivative. `fderiv ℝ ... x` is a continuous linear map E→ℝ, and the outer norm is its operator norm. The statement is not an assertion that the norm is smooth, or differentiable everywhere. The source's surrounding Radial section contributes the implicit type E and its NormedAddCommGroup instance; further structures appear explicitly in the declaration.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

Download module (.lean)

theorem fderiv_norm_div_bound [NormedSpace ℝ E] {R : ℝ} (hR : 0 < R) (x : E) :
    ‖fderiv ℝ (fun y : E => ‖y‖ / R) x‖ ≤ 1 / R

Exact module and namespace context

Proof roadmap

1Prove a global Lipschitz estimate from the reverse triangle inequality
The reverse triangle inequality bounds the change of the norm by the distance between points. Dividing by the positive radius gives Lipschitz constant 1/R.
2Pass the Lipschitz constant to the totalized derivative
Mathlib bounds the norm of fderiv by a global Lipschitz constant. Where a derivative exists, this is the ordinary derivative estimate. Where it does not exist, the totalized derivative is zero, which also satisfies the nonnegative bound.

Full assumptions and notation

All objects and hypotheses

E is a normed additive commutative group equipped with a real normed-vector-space structure.
R∈ℝ with R>0; x∈E is arbitrary.
D_tot denotes fderiv: the Fréchet derivative when it exists and zero when it does not.

Mathematical proof

1. Prove a global Lipschitz estimate from the reverse triangle inequality

The reverse triangle inequality bounds the change of the norm by the distance between points. Dividing by the positive radius gives Lipschitz constant 1/R.

\[\left|\frac{\|y\|}{R}-\frac{\|z\|}{R}\right|=\frac{|\|y\|-\|z\||}{R}\le\frac{\|y-z\|}{R}=\frac1R\,d(y,z).\]

Corresponding Lean step

LipschitzWith.of_dist_le_mul fun y z => by ...; have hnorm : |‖y‖ - ‖z‖| ≤ ‖y - z‖ := abs_norm_sub_norm_le y z; rw [hdiv, abs_div, abs_of_pos hR]; ... div_le_div_of_nonneg_right hnorm hR.le

2. Pass the Lipschitz constant to the totalized derivative

Mathlib bounds the norm of fderiv by a global Lipschitz constant. Where a derivative exists, this is the ordinary derivative estimate. Where it does not exist, the totalized derivative is zero, which also satisfies the nonnegative bound.

\[\|D_{\mathrm{tot}}(\|\cdot\|/R)(x)\|_{\mathrm{op}}\le\operatorname{Lip}(\|\cdot\|/R)\le1/R.\]

Corresponding Lean step

exact norm_fderiv_le_of_lipschitz ℝ hLip

Lean verification

The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.

Lean proof · fderiv_norm_div_bound

Actual proof outline: Prove a global Lipschitz estimate from the reverse triangle inequality: `hLip` packages exactly this inequality. The nonnegative real constant is stored as `⟨1 / R, by positivity⟩`; the omitted algebra is shown in the complete adjacent proof. Pass the Lipschitz constant to the totalized derivative: The library theorem is deliberately stated for totalized fderiv; it requires no `DifferentiableAt` premise. This matters in particular at the origin.

Download module (.lean)

theorem fderiv_norm_div_bound [NormedSpace ℝ E] {R : ℝ} (hR : 0 < R) (x : E) :
    ‖fderiv ℝ (fun y : E => ‖y‖ / R) x‖ ≤ 1 / R := by
  have hLip : LipschitzWith ⟨1 / R, by positivity⟩ (fun y : E => ‖y‖ / R) :=
    LipschitzWith.of_dist_le_mul fun y z => by
      have hnorm : |‖y‖ - ‖z‖| ≤ ‖y - z‖ := abs_norm_sub_norm_le y z
      simp only [Real.dist_eq]
      have hdiv : ‖y‖ / R - ‖z‖ / R = (‖y‖ - ‖z‖) / R := by ring
      rw [hdiv, abs_div, abs_of_pos hR]
      calc
        |‖y‖ - ‖z‖| / R ≤ ‖y - z‖ / R :=
          div_le_div_of_nonneg_right hnorm hR.le
        _ = 1 / R * ‖y - z‖ := by ring
        _ = 1 / R * dist y z := by rw [dist_eq_norm]
  exact norm_fderiv_le_of_lipschitz ℝ hLip

Exact module and namespace context

Scope and omitted-condition boundaries

No inner-product, finite-dimensionality, or nonzero-point hypothesis is present.
Do not read totalized fderiv as a proof of differentiability at the origin or at other nonsmooth points of a general norm.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

LipschitzWith.of_dist_le_mul
abs_norm_sub_norm_le
norm_fderiv_le_of_lipschitz
fderiv_zero_of_not_differentiableAt

Mathematical sources

Current ASTIS declaration and complete body — Authority for the statement, local assumptions, and actual proof/construction documented here.
Existing module card — Existing curated entry for this declaration. Attribution is preserved as local card evidence only, without a new external-source audit or source-equivalence verdict.
norm_fderiv_le_of_lipschitz — Exact checked local Mathlib dependency definition or theorem.
fderiv_zero_of_not_differentiableAt — Explanatory library dependency behind totalization, not necessarily a direct call in this ASTIS body.
Existing test source — Existing direct example invocation inspected; no build or test run was performed.

Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.