Ported for Lean Pool: imports relocated and code adapted to Lean/Mathlib v4.34.0.
Second-order jets of separated functions (BlockBounds) #
Part of the development recording the ordinary two-sided jet consequences of
writing a function on R^n × R^n as a separated difference. Split from
SeparatedJets.lean; see the umbrella module docstring.
The left component of a two-sided jet of a separated difference is a two-sided jet of the left function.
In quantified mathematical form, let G, H : R^n -> R, let
F(ξ, η) = G(ξ) - H(η), and suppose (p, Z) belongs both to the ordinary
superjet and to the ordinary subjet of F at (x0, y0). Then the left
component of p and the left-left block of Z belong both to the ordinary
superjet and to the ordinary subjet of G at x0.
The right component of a two-sided jet of a separated difference is a two-sided jet of the right function with the signs dictated by subtraction.
In quantified mathematical form, let G, H : R^n -> R, let
F(ξ, η) = G(ξ) - H(η), and suppose (p, Z) belongs both to the ordinary
superjet and to the ordinary subjet of F at (x0, y0). Then the negative
right component of p and the negative right-right block of Z belong both
to the ordinary superjet and to the ordinary subjet of H at y0.
A two-sided jet of a separated difference gives the two corresponding one-function two-sided jets.
In quantified mathematical form, let G, H : R^n -> R, let
F(ξ, η) = G(ξ) - H(η), and suppose (p, Z) belongs both to the ordinary
superjet and to the ordinary subjet of F at (x0, y0). Then the left
component of (p, Z) is an ordinary two-sided second-order jet of G at
x0, and the negative right component of (p, Z) is an ordinary two-sided
second-order jet of H at y0.
A two-sided jet of a separated difference has zero mixed Hessian bilinear expression.
In quantified mathematical form, let G, H : R^n -> R, let
F(ξ, η) = G(ξ) - H(η), and suppose that F has an ordinary two-sided
second-order jet (p, Z) at (x0, y0). Then for every x, y ∈ R^n,
⟪Z(x, 0), (0, y)⟫ + ⟪Z(0, y), (x, 0)⟫ = 0.
A Hermitian two-sided jet Hessian of a separated difference is block diagonal.
In quantified mathematical form, let G, H : R^n -> R, let
F(ξ, η) = G(ξ) - H(η), and suppose that F has an ordinary two-sided
second-order jet (p, Z) at (x0, y0). If Z is Hermitian, then the
block-coordinate form of Z is
[X 0; 0 -Y],
where X is the left-left block of Z and Y is the negative of the
right-right block of Z.
A convergent sequence of separated two-sided jet Hessians has a block diagonal limit.
In quantified mathematical form, let G, H : R^n -> R, let
F(ξ, η) = G(ξ) - H(η), and suppose that for every natural number k,
(J_k.gradient, J_k.hessian) is an ordinary two-sided second-order jet of
F at z_k. Suppose also that every J_k.hessian is Hermitian and that a
subsequence of the Hessians converges to Z. Then the block-coordinate form
of Z is
[X 0; 0 -Y],
where X is the left-left block of Z and Y is the negative of the
right-right block of Z.
Closed semijets and matrix bounds for the compact regularized doubled convolution, using the block diagonal limit supplied by selected two-sided jets.
In quantified mathematical form, let K and L be nonempty compact subsets
of R^n, let u be upper semicontinuous on K, and let v be lower
semicontinuous on L. Let
F(ξ, η) = compactSupConvolution lambda K u ξ - compactInfConvolution lambda L v η.
Suppose that a sequence of ordinary two-sided second-order jets of F has
Hermitian Hessians whose subsequence converges to Z, and suppose that
(0, Z) belongs to the closed superjet of F at (0, 0). If the
block-coordinate matrix of Z lies between lower and upper, then
(0, X) belongs to the closed superjet at 0 of the compact
sup-convolution, (0, Y) belongs to the closed subjet at 0 of the compact
inf-convolution, and
lower ≤ [X 0; 0 -Y] ≤ upper,
where X is the left-left block of Z and Y is the negative of the
right-right block of Z.
Transfer the closed semijets produced for compact sup- and inf-convolutions back to the original functions at the origin.
In quantified mathematical form, assume the hypotheses of
closedSemijets_and_blockBounds_of_tendsto_twoSidedJet_regularizedDoubledConvolution
and assume lambda ≠ 0. Since the closed semijets produced at the origin
have first-order part zero, the compact sup-convolution transfer point is
0 + lambda^{-1} 0 = 0, and the compact inf-convolution transfer point is
0 - lambda^{-1} 0 = 0. Hence the same matrices give a closed superjet of
u at 0 relative to K and a closed subjet of v at 0 relative to L,
with the same Loewner bounds.
Selected ordinary two-sided jets for the compact regularized doubled convolution, with Hessian bounds in block coordinates.
In quantified mathematical form, let K and L be nonempty compact subsets
of R^n, let u be upper semicontinuous on K, and let v be lower
semicontinuous on L. Let
F(ξ, η) = compactSupConvolution lambda K u ξ - compactInfConvolution lambda L v η.
Assume 0 ≤ lambda, let B be a symmetric block Hessian, and suppose that
(ξ, η) ↦ F(ξ, η) - (1 / 2)⟪B(ξ, η), (ξ, η)⟫
has a maximum at (0, 0) on all of R^n × R^n. Then there are points
z_k ∈ R^(n+n), ordinary two-sided jets J_k of z ↦ F(z_1, z_2) at
z_k, a matrix Z, and a strictly increasing map φ : Nat -> Nat such
that (J_{φ(k)}).hessian -> Z,
(0, Z) ∈ \overline J^{2,+}_{R^(n+n)}(z ↦ F(z_1,z_2))(0), and
-lambda [I 0; 0 I] ≤ pointHessianToBlockHessian Z ≤ B.
The theorem-shaped proposition for the selected two-sided-jet input used by the compact regularized doubled convolution argument.
In quantified mathematical form, this says that for every lambda ≥ 0, every
pair of nonempty compact sets K, L ⊆ R^n, every function u upper
semicontinuous on K, every function v lower semicontinuous on L, every
Hermitian block matrix B, and every maximum at 0 of
`q ↦ regularizedDoubledConvolution lambda K L u v q
- (1 / 2)⟪Bq, q⟫`,
there exist points z_k ∈ R^(n+n), ordinary two-sided jets J_k at z_k,
a matrix Z, and a strictly increasing map φ : Nat -> Nat such that
(J_{φ(k)}).hessian converges to Z, the jet (0, Z) belongs to the closed
superjet at 0 of the regularized doubled convolution, and the block form of
Z lies between -lambda [I 0; 0 I] and B in the Loewner order.
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 selected two-sided-jet theorem for the compact regularized doubled convolution.
The selected two-sided-jet theorem for the compact regularized doubled
convolution follows from the localized Aleksandrov second-differentiability
theorem in dimension n + n, because the localized Jensen contact-set theorem
has already been proved.
Closed semijets of the original compact functions obtained from the Aleksandrov--Jensen selected ordinary two-sided jets.
In quantified mathematical form, assume the hypotheses of
exists_twoSidedJet_sequence_subsequence_graph_tendsto_regularizedDoubledConvolution
and assume lambda ≠ 0. Then there exist matrices X and Y such that
(0, X) ∈ \overline J^{2,+}_K u(0),
(0, Y) ∈ \overline J^{2,-}_L v(0),
and
-lambda [I 0; 0 I] ≤ [X 0; 0 -Y] ≤ B.
Closed semijets of the original compact functions from the selected two-sided-jet theorem.
In quantified mathematical form, this is
closedSemijets_and_blockBounds_original_of_regularizedDoubledConvolution_max
with the selected two-sided-jet theorem supplied directly, rather than
through the localized Jensen and Aleksandrov inputs.