Ported for Lean Pool: imports relocated and code adapted to Lean/Mathlib v4.34.0.
Aleksandrov--Jensen theorem for semiconvex functions (ContactSelection) #
Part of the Aleksandrov--Jensen development assembling the localized Jensen
contact-set theorem with Aleksandrov differentiability. Split from
SemiconvexJensen.lean; see the umbrella module docstring.
Jensen's lemma for semiconvex functions, stated as the contact-set theorem from the source paper.
In quantified mathematical form, if f : R^n -> R is semiconvex and x0 is
a strict local maximum point of f, then for every r > 0 and every
delta > 0, the set of points x ∈ B(x0, r) for which there exists
p ∈ B(0, delta) such that y ↦ f y + p · y has a local maximum at x
has positive Lebesgue measure.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Jensen's contact-set theorem together with Aleksandrov's theorem supplies a contact point where a second-order jet exists.
Jensen's contact-set theorem on a closed ball together with the localized Aleksandrov theorem supplies a contact point where a second-order jet exists.
Unpacked form of exists_contactPoint_hasSomeSecondOrderJet.
In quantified mathematical form, under Jensen's contact-set theorem and
Aleksandrov's theorem, if f is semiconvex and has a strict local maximum at
x0, then for every r > 0 and delta > 0 there exist x, q, a, and
X such that
Unpacked form of exists_contactPoint_hasSomeSecondOrderJet_closedBall.
In quantified mathematical form, under the localized Jensen contact-set
theorem and localized Aleksandrov theorem, if f is semiconvex on
closedBall x0 r, has a strict local maximum at x0, 0 < r, and
0 < delta, then there exist x, q, a, and X such that
At a contact point provided by Jensen's contact-set theorem and Aleksandrov's differentiability theorem, the local-maximum calculus theorem gives the first- and second-order inequalities.
At a contact point supplied by the localized Jensen and Aleksandrov theorems, the local-maximum calculus theorem gives the first- and second-order inequalities.
The contact-point data for the strictified quadratic objective used in the convex matrix theorem.
Localized unpacked source-proof data for the strictified quadratic objective.
In quantified mathematical form, assume the localized Jensen contact-set
theorem, the localized Aleksandrov theorem, g is convex on R^n, and
x ↦ g x - (1 / 2) * ⟪B x, x⟫ has a maximum at 0 on all of R^n. Then
for every r > 0 and every delta > 0 there exist x, q, a, and X
such that x ∈ closedBall 0 r, q ∈ ball 0 delta, X is Hermitian,
y ↦ strictifiedQuadraticObjective g B y + q · y has a local maximum at
x, and (a, X) is a second-order jet of strictifiedQuadraticObjective g B
at x.
At a contact point for the strictified quadratic objective, the local-maximum calculus theorem gives the first- and second-order inequalities.
Localized source-proof data for the strictified quadratic objective, together with the local-maximum calculus conclusions.
Source-proof data for the strictified quadratic objective, expressed as closed superjet data for the original function.
In quantified mathematical form, assume Jensen's contact-set theorem,
Aleksandrov's differentiability theorem, semiconvexity of
x ↦ g x - (1 / 2) * ⟪B x, x⟫ - (∑ i, x_i^2)^2, and that
x ↦ g x - (1 / 2) * ⟪B x, x⟫ has a maximum at 0. Then for every
r > 0 and every delta > 0 there exist x, q, a, and X such that
x ∈ closedBall 0 r, q ∈ ball 0 delta, X is Hermitian,
a + q = 0, X ≤ 0, and after adding the coordinate-quartic jet at x
and the recentered quadratic jet at x, the resulting jet belongs to
\overline J^{2,+}_{R^n} g(x). Its Hessian component is at most
B + (coordinate-quartic Hessian at x) in the Loewner order.
Localized source-proof data for the strictified quadratic objective, expressed as closed superjet data for the original function.
In quantified mathematical form, assume the localized Jensen contact-set
theorem, the localized Aleksandrov theorem, g is convex on R^n, and
x ↦ g x - (1 / 2) * ⟪B x, x⟫ has a maximum at 0. Then for every
r > 0 and every delta > 0 there exist x, q, a, and X such that
x ∈ closedBall 0 r, q ∈ ball 0 delta, X is Hermitian, a + q = 0,
X ≤ 0, and after adding the coordinate-quartic jet at x and the
recentered quadratic jet at x, the resulting jet belongs to
\overline J^{2,+}_{R^n} g(x). Its Hessian component is at most
B + (coordinate-quartic Hessian at x) in the Loewner order.
Localized selected closed-superjet data with explicit estimates on the base point and first-order component.
In quantified mathematical form, under the same hypotheses as
exists_strictifiedQuadraticObjective_closedSuperjet_data_closedBall, for
every r > 0 and every delta > 0 there exist x, a, and a jet J such
that
Localized selected closed-superjet data with norm bounds and Hermitian selected Hessian.
In quantified mathematical form, this is the preceding selected-data theorem
with the additional conclusion that the Hessian component of the produced
closed-superjet jet is Hermitian, assuming the quadratic matrix B is
Hermitian.
Selected closed-superjet data along the sequence 1 / (k + 1).
In standard mathematical terms, under the hypotheses of the localized
Aleksandrov--Jensen selected-data theorem, one can choose, for every natural
number k, a point x_k, a vector a_k, a Hessian X_k, and a closed
superjet J_k ∈ \overline J^{2,+}_{R^n} g(x_k) such that
‖x_k‖ ≤ 1 / (k + 1), ‖a_k‖ < 1 / (k + 1),
and therefore x_k -> 0 and a_k -> 0. The theorem also records the exact
formula for J_k and the Hessian upper bound used in the limiting argument.