Ported for Lean Pool: imports relocated and code adapted to Lean/Mathlib v4.34.0.
Cube-local second-order assembly #
This file records the final measure-theoretic assembly step in the source cube proof. The
remaining mathematical work is pointwise: turn the source-route gradient expansion at a good point
into SecondOrderDifferentiableAt. Once that pointwise bridge is available, the a.e. cube
statement follows immediately from the countable good-set/envelope theorem.
At a source good point, every subgradient on the ambient source cube is the Fréchet gradient.
This is the base-point input in the source subgradient-extension argument. The point x belongs
to Q_1, hence has a neighborhood inside Q_3, and membership in the good set includes
Fréchet differentiability at x.
Cube-local subgradient extension from cluster-gradient density.
This is the source subgradient-extension lemma with the hard convex-analysis input exposed as
hdensity. The estimate hgradient is the moving-base gradient estimate produced from the
good-point gradient expansion in the LaTeX proof.
Good-point version of the cube-local subgradient extension.
The abstract cluster-gradient bridge requires a separate base-point uniqueness hypothesis. At a good point this is automatic, because the good set records differentiability at the base point.
Good-point subgradient extension from the source-route gradient little-o expansion.
This is the cube-local form needed after the Lipschitz-envelope step: the envelope argument
produces a little-o expansion of frechetGradient u along the dense differentiability set
D_{3/2}. The generic moving-base lemma converts that into the punctured estimates required by
the cluster-gradient subgradient bridge. The remaining hypothesis is exactly the source
finite-dimensional density theorem for subgradients.
Good-point subgradient extension from gradient expansion and directional halfspace tests.
This is the current source-facing form of the remaining cluster-density step. Instead of asking
directly for membership in the closed convex hull of gradient cluster values, it asks for the
separating-halfspace consequence: every linear upper bound valid on the gradient cluster set is
valid for each nearby subgradient. The closed-convex-hull membership is then supplied by the
clusterDensity_of_eventually_forall_inner_le helper.
Good-point subgradient extension from gradient expansion and directional cluster domination.
This is the source-facing form closest to the one-dimensional convex argument: for each nearby
punctured point y, every subgradient directional value p · z is dominated by some cluster
gradient directional value q · z. The halfspace and closed-convex-hull conclusions are then
formal consequences.
Good-point subgradient extension from gradient expansion and right-derivative cluster domination.
This separates the remaining one-dimensional convex-analysis input from the already-formalized
subgradient inequality p · z <= D_+ (u(y + t z))|_{t = 0}. It remains to prove that the right
derivative is dominated by a directional value of some nearby gradient cluster value.
Auxiliary good-point wrapper from positive-line gradient clusters.
This theorem is useful as a filter-transport interface, but it is not the active source route.
For a full-measure differentiability set, one should not expect every affine line through every
nearby y and direction z to contain differentiability points accumulating at y.
Auxiliary positive-line wrapper with line right-derivative realization along the same filter.
This is parked as a non-source-route interface: the source proof uses ambient subgradient-density
from gradients approaching y, not existence of linewise differentiability clusters for every
direction.
Along the source differentiability set, the line-restricted right derivative is eventually realized by the Fréchet gradient directional component.
Auxiliary wrapper reducing positive-line cluster realization to positive-line cluster existence.
The realization part is automatic on the differentiability-set filter, but the remaining existence hypothesis is generally too strong for the main Aleksandrov route. The source-aligned boundary remains the ambient closed-convex-hull cluster-density theorem.
Segment form of cube-local subgradient linearization at a good point.
This is the estimate used by the source proof before integrating along
s ↦ u (x + s • z): after shrinking z, every point of the segment lies in Q_{3/2}, and every
subgradient there is modeled by frechetGradient u x + B (s • z) up to
ε * ‖s • z‖.
Scalar directional form of cube-local segment subgradient linearization.
This is the estimate that feeds the source proof's right-derivative/integration calculation:
after pairing each segment subgradient with the segment direction z, the error from the affine
function inner (frechetGradient u x) z + t * inner z (B z) is bounded by
ε * ‖z‖ ^ 2.
Good-point Taylor expansion from subgradient linearization and the source line-derivative bridge.
This packages the final integration step after the segment subgradient estimate. The remaining
line hypotheses are intentionally explicit: convexity supplies the right-derivative integral
representation and integrability, while the source support-function identity supplies
hrightSubgradient.
For a good point x ∈ Q_1, all sufficiently short source increments have their whole
unit parameter interval inside the interior of the line domain for Q_3.
Convex line-restriction right-derivative integrability on the unit segment, eventually in the source increment.
Convex line-restriction right-derivative FTC representation on the unit segment, eventually in the source increment.
For a good point x ∈ Q_1, all sufficiently short nontrivial segment parameters lie in the
ambient interior of Q_3.
Symmetric-operator version of
cubeGoodSet_hasSecondOrderExpansionAt_of_lineRightDeriv, yielding the project
SecondOrderDifferentiableAt predicate.
Good-point second-order differentiability from subgradient linearization and the source line-derivative bridge.
This version does not require a separate symmetry proof for B; the symmetric part of B has
the same quadratic form and is used in the final SecondOrderDifferentiableAt witness.
Good-point second-order differentiability from subgradient linearization and the line-subgradient lift interface.
This lower-level compatibility form of the final integration step keeps the vector-valued line-subgradient lift as an explicit hypothesis. The preferred wrapper below supplies the lift from strict-epigraph separation.
Good-point second-order differentiability from subgradient linearization and the functional line-subgradient lift interface.
This lower-level compatibility form keeps the functional line-subgradient lift as an explicit hypothesis. The preferred wrapper below supplies it from Mathlib Hahn-Banach separation.
Good-point second-order differentiability from subgradient linearization alone.
The line-subgradient ambient lift is supplied by the strict-epigraph separation theorem in
ConvexOn.lineSubgradientLiftsToAmbientFunctional_of_isOpen, so no separate Hahn-Banach
hypothesis remains at this point.