Ported for Lean Pool: imports relocated and code adapted to Lean/Mathlib v4.34.0.
Cube-local Lipschitz-envelope squeeze lemmas #
This file isolates the source proof's final envelope argument. Once the coordinate gradient function is squeezed between two Lipschitz envelopes with the same derivative at a good point, the coordinate gradient has the corresponding first-order expansion along the differentiability set.
If U \ D is null and U is open, then U ∩ D is dense in U.
This is the local form of the source proof's statement that a full-measure subset of an open cube is dense in that cube.
Differentiability points of u inside the source cube Q_r.
Equations
Instances For
The differentiability points in Q_1 are dense enough for the envelope argument on Q_1.
The differentiability points in Q_{3/2} are dense enough for the envelope argument on
Q_1.
The density theorem gives a nontrivial differentiability-point sampling filter at each point
of Q_1, with sampling still inside Q_1.
The density theorem gives a nontrivial differentiability-point sampling filter at each point
of Q_1.
The good set Omega_m lies in the differentiability set D_{3/2} used for envelopes.
The good set Omega_m lies in the working cube Q_1.
Lower boundedness of a coordinate of the gradient on D_{3/2}.
Upper boundedness of a coordinate of the gradient on D_{3/2}.
Cross-estimate input for the coordinate-gradient envelope argument.
The lower McShane-type envelope used in the source proof:
inf_y (g y + K * dist x y) over y ∈ E.
Equations
- AleksandrovDifferentiability.lowerMcShaneEnvelope K E g x = ⨅ (y : ↑E), g ↑y + ↑K * dist x ↑y
Instances For
The upper McShane-type envelope, defined by duality from the lower envelope.
Equations
- AleksandrovDifferentiability.upperMcShaneEnvelope K E g x = -AleksandrovDifferentiability.lowerMcShaneEnvelope K E (fun (y : AleksandrovDifferentiability.SourceCubeSpace n) => -g y) x
Instances For
A bounded-below lower McShane envelope is globally Lipschitz with the same constant.
The proof is the standard source-envelope estimate: compare every cone based at y using the
triangle inequality, then pass to the infimum.
The lower envelope is bounded above by every defining cone.
A bounded-above upper McShane envelope is globally Lipschitz with the same constant.
Every defining cone lies below the upper envelope.
The lower envelope agrees with g at points where the source cross estimate is based.
The upper envelope agrees with g at points where the source cross estimate is based.
Lower-envelope increments are below the original increments at cross-estimate base points.
Original increments are below upper-envelope increments at cross-estimate base points.
The concrete envelopes are ordered on the defining set E.
By continuity, the concrete envelopes are ordered on closure E.
Local order of the concrete envelopes near points in an open set contained in closure E.
If two differentiable envelopes are ordered near a point and touch at that point, then their derivatives agree there.
This is the Fermat-theorem step in the source proof, applied to gplus - gminus.
Abstract squeeze step for the source proof's Lipschitz envelopes.
In the source notation, gminus and gplus are the lower and upper McShane envelopes of a
coordinate derivative g on the dense differentiability set E. If the two envelopes are
differentiable at x0 with the same derivative ell, and the increments of g are eventually
squeezed between the envelope increments along E, then g has the same first-order expansion
along E.
Packaged touching-envelope squeeze step.
This combines the Fermat-theorem derivative-agreement step with
lipschitzEnvelope_squeeze_expansion. It returns the row vector representing the common
derivative of the two scalar envelopes.
A.e. envelope bridge for a fixed coordinate-gradient function.
Once the lower and upper envelopes are globally Lipschitz, Rademacher gives differentiability of
both envelopes almost everywhere. At points of the touching set F, the touching/squeeze lemma
then gives the first-order expansion of the squeezed function along E.
A.e. envelope bridge with only local order near points of F.
This is the form used by the source proof: the envelopes are ordered on the working open cube,
so they are ordered in a neighborhood of each point of F.
Restricted-measure form of lipschitzEnvelope_ae_touching_squeeze_expansion_of_mem.
Restricted-measure local-order form of
lipschitzEnvelope_ae_touching_squeeze_expansion_of_mem_localOrder.
Concrete McShane-envelope a.e. squeeze wrapper.
After the source proof establishes the remaining order fact g^- <= g^+ for the concrete
envelopes, the boundedness and cross-estimate hypotheses give all other inputs needed by the
abstract a.e. envelope bridge.
Concrete McShane-envelope a.e. squeeze wrapper on an open working set.
This is the source-faithful form: if the working open set U lies in closure E, then density
and continuity provide the local order g^- <= g^+ near every point of F ⊆ U.
Ambient-measure version of
lowerUpperMcShaneEnvelope_ae_squeeze_of_cross_bound_on_open, avoiding a measurability
assumption on the touching set F.
Concrete source-envelope conclusion for one coordinate of the Fréchet gradient on an integer good set.
For almost every ambient point, membership in Omega_m implies that the i-th coordinate of
grad u has a first-order expansion as the variable tends to the point through the
differentiability set D_{3/2}.
Source-envelope output assembled over all coordinates: at almost every point of an integer
good set, the Fréchet gradient has a first-order expansion along D_{3/2}.
Source-route a.e. gradient expansion after choosing an integer good set.
This is the countable-good-set assembly of
cubeGoodSet_nat_ae_frechetGradient_expansion_three_halves_of_mem: the source cover theorem
shows that Q_1 is covered up to a null set by the integer good sets, and the fixed-good-set
envelope theorem supplies the linearization on whichever good set contains the point.