Ported for Lean Pool: imports relocated and code adapted to Lean/Mathlib v4.34.0.
Aleksandrov--Jensen theorem for semiconvex functions (MatrixConclusion) #
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.
Selected data along the sequence 1 / (k + 1), retaining ordinary two-sided
jets of the original function.
In quantified mathematical form, under the hypotheses of the localized
Aleksandrov--Jensen selected-data theorem, there exist sequences x_k,
a_k, X_k, and J_k such that, for every natural number k,
‖x_k‖ ≤ 1 / (k + 1);‖a_k‖ < 1 / (k + 1);X_kand(J_k).hessianare Hermitian;(a_k, X_k)is an ordinary two-sided second-order jet ofx ↦ g x - (1 / 2) * ⟪B x, x⟫ - (∑ i, x_i^2)^2atx_k;J_kis obtained from(a_k, X_k)by adding the coordinate-quartic jet atx_kand the recentered quadratic jet atx_k;J_kbelongs to the closed superjet ofgatx_k;(J_k).hessian ≤ B + (coordinate-quartic Hessian at x_k);(J_k).gradientand(J_k).hessianform an ordinary two-sided second-order jet ofgatx_k.
Moreover x_k -> 0 and a_k -> 0 as k -> ∞.
Selected closed-superjet data together with a convergent Hessian subsequence.
In standard mathematical terms, under the hypotheses of the localized
Aleksandrov--Jensen selected-data theorem, one may choose selected points
x_k, first-order vectors a_k, auxiliary Hessians X_k, and closed
superjets J_k ∈ \overline J^{2,+}_{R^n} g(x_k) as in
exists_strictifiedQuadraticObjective_closedSuperjet_sequence_norm_bounds_hessian.
Moreover, the Hessian matrices (J_k).hessian have a convergent subsequence.
Selected closed-superjet data with a Hessian subsequential limit satisfying the matrix-order bounds required in the Aleksandrov--Jensen theorem.
In standard mathematical terms, the selected Hessians admit a subsequential
limit Z, and this limit is Hermitian, nonnegative, and bounded above by the
quadratic matrix B.
The gradient components of the selected closed-superjet sequence converge to zero along every strictly increasing subsequence.
In standard mathematical terms, if
J_k = (a_k, X_k) + coordinateQuarticJetAt x_k + quadraticModelJetAt 0 0 B x_k,
x_k -> 0, and a_k -> 0, then (J_{φ(k)}).gradient -> 0 for every
strictly increasing φ : Nat -> Nat.
Convergence of jets follows from convergence of their gradient and Hessian components.
Selected closed-superjet data with convergence of the graph coordinates needed for the closed-superjet graph argument.
In standard mathematical terms, the selected subsequence may be chosen so that
x_{φ(k)} -> 0, g(x_{φ(k)}) -> g(0), and
J_{φ(k)} -> (0, Z), where Z is Hermitian and satisfies 0 ≤ Z ≤ B.
Selected closed-superjet data with graph convergence and ordinary two-sided jets of the original function.
In quantified mathematical form, under the hypotheses of
exists_strictifiedQuadraticObjective_closedSuperjet_sequence_subsequence_graph_tendsto,
the selected sequences may also be chosen so that, for every natural number
k, (J_k).gradient and (J_k).hessian form an ordinary two-sided
second-order jet of g at x_k.
Selected ordinary two-sided jets for a semiconvex function.
In quantified mathematical form, let f : R^n -> R be continuous and suppose
that f satisfies the coordinate semiconvexity inequality on all of R^n
with constant lambda ≥ 0. Let B be a symmetric matrix, and suppose that
has a maximum at 0 on all of R^n. Then there are points x_k, jets
J_k, a matrix Z, and a strictly increasing map φ : Nat -> Nat such that:
- for every
k,J_kis an ordinary two-sided second-order jet offatx_k; - the Hessians
(J_{φ(k)}).hessianconverge toZ; (0, Z)belongs to the closed superjet offat0;-lambda I ≤ Z ≤ B.
The convex-function form of the Aleksandrov--Jensen matrix theorem.
In quantified mathematical form, this says that for every continuous convex
function g : R^n -> R and every Hermitian matrix B, if
x ↦ g x - (1 / 2) * ⟪B x, x⟫ has a maximum at 0 on all of R^n, then
there exists a Hermitian matrix Z such that
(0, Z) ∈ \overline J^{2,+}_{R^n} g(0) and 0 ≤ Z ≤ B.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The localized Jensen contact-set theorem and localized Aleksandrov second-differentiability theorem imply the convex Aleksandrov--Jensen matrix theorem.
The localized Jensen contact-set theorem has already been proved in this file, so the convex Aleksandrov--Jensen matrix theorem follows from the localized Aleksandrov second-differentiability theorem alone.
The Aleksandrov--Jensen semiconvex matrix theorem in the convexified form.
In quantified mathematical form, this is the statement: for every continuous
f : R^n -> R and every Hermitian matrix B, if 0 ≤ lambda, if
x ↦ f x + (lambda / 2) * ∑ i, x_i^2 is convex on all of R^n, and if
x ↦ f x - (1 / 2) * ⟪B x, x⟫ has a maximum at 0 on all of R^n, then
there exists a Hermitian matrix X such that
(0, X) ∈ \overline J^{2,+}_{R^n} f(0) and -lambda I ≤ X ≤ B.
Equations
Instances For
The convex-function Aleksandrov--Jensen theorem implies the semiconvex
Aleksandrov--Jensen theorem for each constant lambda.
In quantified mathematical form, apply the convex theorem to
g x = f x + (lambda / 2) * ∑ i, x_i^2 and the matrix B + lambda I. The
closed-superjet conclusion for g is then transformed into the corresponding
closed-superjet conclusion for f by subtracting the quadratic jet.
The convex-function Aleksandrov--Jensen theorem implies the family of semiconvex theorem statements for all constants.
The public Aleksandrov--Jensen theorem target implies the coordinate semiconvex formulation used in the comparison files.
The coordinate semiconvex formulation and the public convexified Aleksandrov--Jensen formulation are equivalent.
Apply the public Aleksandrov--Jensen theorem target to a compact sup-convolution.