Ported for Lean Pool: imports relocated and code adapted to Lean/Mathlib v4.34.0.
Line-integral endpoint estimates #
This file packages the calculus bookkeeping used at the final Taylor-expansion step of the
Aleksandrov proof. Once a line-restriction increment is represented by an integral whose
integrand is uniformly close to the affine model
inner ℝ p z + t * inner ℝ z (B z), the endpoint affine remainder is close to the quadratic
model (1 / 2) * inner ℝ z (B z).
Line-restriction version of interval-integrability of the right derivative on an interval contained in the interior line domain.
Line-restriction version of the right-derivative FTC identity on an interval contained in the interior line domain.
Endpoint-subtraction orientation of
ConvexOn.lineRestriction_integral_rightDeriv_eq_sub_of_uIcc_subset_interior.
Ambient endpoint form of the unit-interval integration estimate.
In the source proof this is the last line-segment integration step: for
φ(t) = u (x + t • z), a uniform model bound on the derivative-like integrand by
p · z + t z · B z gives the quadratic Taylor remainder estimate at x + z.
Right-derivative specialization of
norm_affineRemainder_sub_quadratic_le_of_line_integral_model_bound.
This is the form closest to the source proof's notation
φ'_+(t) = sup {p · z : p ∈ ∂u(x + t z)}. The hypotheses deliberately keep the
one-dimensional FTC representation and integrability explicit; later convex-analysis lemmas
should supply them for sufficiently short segments.
Convert subgradient linearization along a segment into the right-derivative endpoint quadratic estimate, assuming the source proof's support-function identity is available along the line.
The hypothesis hrightSubgradient is the remaining convex-analysis bridge in this local form:
for each parameter t ∈ (0,1], the right derivative of the line restriction is realized by
pairing the segment direction with some ambient subgradient at x + t • z.
Version of HasSubgradientLinearizationOnAt.eventually_quadraticBound_of_lineRightDeriv
whose remaining support-function input is stated as a lift of arbitrary line subgradients to
ambient subgradients. Convexity supplies the fact that the right derivative is a line
subgradient.
Functional-lift version of
HasSubgradientLinearizationOnAt.eventually_quadraticBound_of_lineSubgradientLift.
This is the form intended for the eventual separation proof: the ambient lift of each line
subgradient may be supplied by a supporting continuous linear functional, and Fréchet-Riesz
converts it to the vector-valued subgradient used by SubgradientOn.
Expansion form of
HasSubgradientLinearizationOnAt.eventually_quadraticBound_of_lineRightDeriv.
This is the local Taylor conclusion before the separate symmetry requirement needed by
SecondOrderDifferentiableAt.
Expansion form using the line-subgradient lift interface.
Expansion form using the functional line-subgradient lift interface.
Second-order differentiability form of
HasSubgradientLinearizationOnAt.hasSecondOrderExpansionAt_of_lineRightDeriv.
The operator produced by gradient linearization need not be separately shown symmetric here:
SecondOrderDifferentiableAt is obtained using its symmetric part, which has the same quadratic
form.
Second-order differentiability form using the line-subgradient lift interface.
As in the right-derivative version, the symmetric part of the linearized operator is used for the final Hessian witness.
Second-order differentiability form using the functional line-subgradient lift interface.