Ported for Lean Pool: imports relocated and code adapted to Lean/Mathlib v4.34.0.
Cube-local good-set coverage #
This file packages the source proof's countable good-set cover
Q_1 = ⋃_m Omega_m up to a null set, after first differentiability a.e. and finite
upper-contact opening a.e. have been established.
At a source good point, the slope in the upper-contact trap can be normalized to the
Fréchet gradient. This is the cube-local form of the source proof's choice
p_0 = grad u(x_0).
Source-good-point affine-remainder trap with the Fréchet-gradient slope.
Source-good-point directional comparison for gradients.
If x0 is good and x1 is a differentiability point, convexity at x1 and the good-point
quadratic trap at x0 control the component of grad u x1 - grad u x0 in any tested
direction whose endpoint remains in Q_3.
Directional comparison for gradients when the second point is any interior point of Q_3.
This is the domain-flexible form needed for the source proof's later use of differentiability
points in Q_{3/2} rather than only in Q_1.
Directional gradient control near a source good point, before optimizing over directions.
The small-distance hypothesis keeps the tested point x1 + ‖x1 - x0‖ • v inside Q_3, using
x0 ∈ Q_1.
Norm form of the local gradient control near a source good point.
Directional gradient control near a source good point for differentiability points in
Q_{3/2}.
This is the source-local version used before the Lipschitz-envelope argument: the second point is
allowed to lie in Q_{3/2}, and the small-distance hypothesis keeps the tested endpoint in
Q_3.
Norm form of the local gradient control for differentiability points in Q_{3/2}.
Full source-local gradient control for differentiability points in Q_{3/2}, including the
coarse-distance case. This is the cross-set estimate used before the Lipschitz-envelope
argument, with A = m and the oscillation term included for the large-distance case.
Coordinate form of the global Q_{3/2} gradient-control estimate. This is the exact
cross-set Lipschitz hypothesis used for the source proof's envelope functions
g_i = partial_i u on D_{3/2}.
Integer-indexed good-set version of the local gradient control.
This is the form used for the countable good-set cover: choose A = m and absorb the
arbitrary η > 0 by taking η = 1.
Pairwise gradient control on an integer good set, localized to a small closed ball.
The radius 1 / 4 ensures any two localized points are within distance 1 / 2, exactly the
small-distance hypothesis needed by cubeGoodSet_nat_norm_gradient_sub_le.
The Fréchet-gradient map is Lipschitz on each localized integer good set.
This is the Rademacher-ready packaging of the source proof's good-set gradient estimate.
Rademacher bridge for the localized integer good set.
This form avoids a measurability side condition on cubeGoodSet: for almost every ambient point,
membership in the localized good set implies differentiability of the gradient within that set.
Restricted-measure Rademacher bridge for a localized integer good set, assuming the localized set has already been made measurable.
This is the exact form needed for the final a.e. assembly once measurability/countable localization of the good sets has been supplied.
On each integer good set, the Fréchet-gradient map is locally Lipschitz.
This is the intrinsic local form of the source proof's gradient-control lemma on Omega_m.
A differentiability-within statement on a localized closed ball transfers back to the whole integer good set when the base point lies in the corresponding open ball.
Countable localized Rademacher bridge over the integer good sets.
If a countable family of radius-1 / 4 closed balls covers Q_1, then for almost every ambient
point, membership in the countable good-set union gives a localized good set on which
frechetGradient u is differentiable within that localized set.
Countable open-ball version of the localized Rademacher bridge.
An open radius-1 / 4 ball cover of Q_1 gives, for almost every point in the countable good-set
union, differentiability of frechetGradient u within the corresponding integer good set itself.
If a point of Q_1 is differentiable and has finite upper-contact opening, then it belongs
to one of the countably many source cube good sets Omega_m.
First differentiability a.e. and finite upper-contact opening a.e. imply that the countable
union of source cube good sets covers Q_1 up to a null set.
Source-route good-set cover from convexity, first differentiability a.e., and the finite upper-contact-opening theorem.
Source-route a.e. gradient differentiability on localized good sets.
This combines the null complement of the countable good-set union with the countable localized
Rademacher bridge. The remaining input is a countable radius-1 / 4 closed-ball cover of Q_1,
which is a purely topological/separability fact.
Source-route a.e. differentiability of the gradient within an integer good set.
This is the open-ball-cover version of
ae_restrict_sourceOpenCube_exists_local_goodSet_frechetGradient_diffWithin: the open cover lets
the localized differentiability-within statement transfer from
Omega_m ∩ closedBall c (1 / 4) back to Omega_m.
The canonical dense sequence gives a countable open radius-1 / 4 ball cover of Q_1.
Source-route a.e. differentiability of the gradient within an integer good set, with the countable open-ball cover chosen from the canonical dense sequence.
Differentiability of the Fréchet-gradient map within a good set gives the corresponding little-o linearization along that good set.
Existential linearization form of differentiability of the Fréchet-gradient map within a
good set. This avoids committing later arguments to a particular representative such as
fderivWithin when the good set is not known to be a unique-differentiability set.
Construct the source-space linear map whose coordinate rows are the vectors ell i.
Assemble coordinate-wise first-order gradient expansions into a vector expansion.
This is the linear-algebra step in the source proof after the Lipschitz-envelope/Rademacher
argument: once each component of frechetGradient u has a first-order expansion with row vector
ell i, any continuous linear map B whose rows are those functionals gives the corresponding
vector-valued little-o expansion.
Existential version of coordinate-to-vector gradient linearization.
The chosen linear map is the row map determined by the coordinate vectors ell i.
Source-route a.e. good-set gradient linearization, with the countable cover chosen from the canonical dense sequence.
This is the Rademacher output in the form needed for the next Aleksandrov step: at almost every
point of Q_1, one can choose an integer good set and a linear map which gives the first-order
expansion of the gradient along that good set.