Ported for Lean Pool: imports relocated and code adapted to Lean/Mathlib v4.34.0.
Cube-local second-order a.e. assembly #
Source-route a.e. second-order differentiability on Q_1, with the subgradient-extension
step reduced to the finite-dimensional cluster-density theorem.
The envelope theorem supplies the good point, the linear map B, and the gradient little-o
expansion. The hypothesis hdensity is the remaining convex-analysis input identifying nearby
subgradients with the closed convex hull of cluster gradients. The hypothesis htaylor is the
last integration step converting subgradient linearization into a second-order Taylor expansion.
Source-route a.e. second-order differentiability on Q_1, reduced to the remaining
source-facing pointwise inputs.
At this boundary the envelope theorem and subgradient-extension bridge have already been used. The remaining hypotheses are the finite-dimensional cluster-density theorem, the right-derivative/support-function identity along short segments. The symmetric part of the linear map selected by the gradient-expansion step supplies the symmetric Hessian witness.
Source-route a.e. second-order differentiability on Q_1, reduced to the cluster-density
theorem and the ambient lift theorem for line subgradients.
This is sharper than
ae_restrict_sourceOpenCube_secondOrderDifferentiableAt_of_clusterDensity_lineRightDeriv: the
one-dimensional fact that the right derivative is a line subgradient has already been discharged,
so the remaining support-function input is stated as a lift of arbitrary line subgradients to
ambient subgradients with the same directional pairing.
Source-route a.e. second-order differentiability on Q_1, reduced to the cluster-density
theorem and an explicit functional ambient lift theorem for line subgradients.
This remains as a compatibility boundary; the direct cluster-density wrapper below supplies the functional lift from strict-epigraph separation.
Source-route a.e. second-order differentiability on Q_1, reduced to the finite-dimensional
cluster-density theorem for convex subgradients.
The line-subgradient lift is no longer an external hypothesis: it is supplied by Mathlib
Hahn-Banach separation through ConvexOn.lineSubgradientLiftsToAmbientFunctional_of_isOpen.
Source-route a.e. second-order differentiability on Q_1, reduced to the directional
halfspace form of the finite-dimensional subgradient cluster-density theorem.
This is the most scalar form of the remaining cube-level input: at good points and nearby
punctured points, each subgradient must satisfy every linear upper bound that holds for all
cluster values of the Fréchet gradient along D_{3/2}.
Source-route a.e. second-order differentiability on Q_1, reduced to directional
dominating cluster values.
This is the current closest formal boundary to the scalar convex proof: each directional value
of each nearby subgradient is bounded above by the same directional value of some cluster
gradient along D_{3/2}.
Source-route a.e. second-order differentiability on Q_1, reduced to the right-derivative
cluster domination theorem along arbitrary directions.
Auxiliary a.e. wrapper reduced to positive-line gradient clusters along arbitrary directions.
This is not the active source route; the linewise cluster hypothesis is stronger than the ambient cluster-density theorem used by the source proof.
Auxiliary a.e. wrapper with positive-line clusters and line right-derivative realization.
This interface is retained for possible reuse, but the main formalization should proceed through ambient subgradient cluster-density.
Auxiliary a.e. wrapper reduced to existence of positive-line gradient clusters.
The right-derivative realization is automatic on the differentiability-set filter, but the linewise cluster-existence hypothesis is not the source theorem and is generally too strong as a main target.
Source-route a.e. second-order differentiability on Q_1, reduced to the pointwise bridge
from good-set gradient expansion to second-order differentiability.
This is the formal version of the last paragraph of the cube proof before global rescaling:
the countable union of good sets covers Q_1 up to a null set, the envelope argument supplies a
linearization of the gradient at almost every good point, and a pointwise theorem converts that
linearization into the second-order Taylor expansion.