Existing in Mathlib · Analysis
Rademacher's Theorem
A globally Lipschitz map between finite-dimensional real normed spaces is Fréchet-differentiable at almost every point with respect to an additive Haar measure on its Borel domain.
- Lipschitz maps
- almost-everywhere differentiability
- Fréchet derivative
- additive Haar measure
- line derivatives
- Morrey's argument
- dense directions
Exact theorem
Exact Mathlib statement
theorem LipschitzWith.ae_differentiableAt {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F] {C : ℝ≥0} {μ : Measure E} [FiniteDimensional ℝ E] [FiniteDimensional ℝ F] [IsAddHaarMeasure μ] {f : E → F} (h : LipschitzWith C f) : ∀ᵐ x ∂μ, DifferentiableAt ℝ f xThe theorem at a glance
Rademacher's theorem at a glance
A visual guide to the theorem's hypotheses, structure, and conclusion; the exact statement gives the formal detail.
Rademacher's theorem at a glance
Detailed visual description
The poster foregrounds the exact μ-almost-everywhere conclusion and keeps the finite-dimensional real normed-space, Borel measurable, additive Haar, and global Lipschitz assumptions visible. A central coordinate fabric distinguishes many regular points with direction fans and local linear-map ellipsoids from sparse exceptional points. Four source-bound movements summarize coordinate reduction, almost-everywhere line differentiability, Morrey linearity, and the dense-direction upgrade to a Fréchet derivative; the footer explicitly excludes everywhere differentiability and stronger smoothness.
Statement structure
From hypotheses to conclusion
This map summarizes the statement's structure; the exact Mathlib declaration remains authoritative.
Local affine approximation almost everywhere
Detailed visual description
A globally Lipschitz map is locally approximated by affine maps at almost every point with respect to the recorded additive Haar measure. Six representative regular neighborhoods carry local direction frames and correspond to affine images of different orientations and scales. A few faint subordinate marks leave room for a possible measure-null exceptional set without asserting that such a set is nonempty or giving it any topology, density, branching structure, or shape.
Why it matters
A mathematical landmark
Rademacher's theorem is a foundational bridge between metric regularity and differential structure: a global Lipschitz bound forces a first-order linear approximation at almost every point. Mathlib's Morrey-style route is especially instructive because it passes from one-dimensional line derivatives through almost-everywhere linearity and dense directions to the full Fréchet derivative.
ProofAtlas record
What has been checked
Mathlib is the source of the theorem; the local Lean replay and page review are separate.
Claim boundary
No new theorem is claimed
This page indexes Mathlib's finite-dimensional real normed-space form of Rademacher's theorem. With E carrying a measurable structure equal to its Borel structure, μ an additive Haar measure on E, E and F finite-dimensional over ℝ, and f : E → F satisfying LipschitzWith C f, the declaration concludes ∀ᵐ x ∂μ, DifferentiableAt ℝ f x. The endpoint is Fréchet differentiability at μ-almost every point, not differentiability everywhere, continuity of the derivative, continuous differentiability, or stronger smoothness.
- The declaration gives Fréchet differentiability at μ-almost every point; it does not claim differentiability at every point.
- The declaration does not claim that the derivative depends continuously on the point, that f is continuously differentiable, or that f has higher regularity.
- The selected theorem is finite-dimensional over ℝ and uses an additive Haar measure μ on the Borel domain E; it is not an infinite-dimensional or measure-free statement.
- ProofAtlas is indexing an existing Mathlib theorem, and generated explanations and visuals are not proof evidence.
Source and local evidence
Where the theorem comes from
- Existing declaration
LipschitzWith.ae_differentiableAtin mathlib- Relationship
- The checked artifact is the upstream declaration itself
- Local Lean evidence
artifact.library.mathlib.rademacher-theorem.v001