Ported for Lean Pool: imports relocated and code adapted to Lean/Mathlib v4.34.0.
Jensen Contact-Set Theorem (VolumeEstimates) #
Part of the localized Jensen contact-set theorem and the smooth convex
approximation machinery used to prove it. Split from Jensen.lean; see the
umbrella module docstring.
The gradient image of the Jensen contact set contains a ball around 0.
In quantified mathematical form, under the hypotheses of the preceding
contact-point selection theorem, if delta > 0, then there exists rho > 0
such that every q ∈ ball 0 rho can be written as q = -G z for some
z ∈ JensenContactSet f x0 r delta.
The gradient image of the closed-ball global contact set contains a ball
around 0.
In quantified mathematical form, under the same hypotheses as
exists_pos_radius_ball_subset_neg_gradient_image_jensenContactSet, if
delta > 0, then there exists rho > 0 such that every q ∈ ball 0 rho
can be written as q = -G z for some
z ∈ JensenGlobalContactSet f x0 r delta.
The explicit boundary-gap radius used in the smooth proof of Jensen's lemma.
In quantified mathematical form, assume every boundary point of
closedBall x0 r satisfies f x ≤ f x0 - gamma, with gamma > 0. If
delta > 0, then every vector in
ball 0 (min (delta / 2) (gamma / (2 * ((n : Real) * r + 1))))
is equal to -G z for some z ∈ JensenGlobalContactSet f x0 r delta.
A measure-theoretic consequence used in the smooth part of Jensen's lemma.
In quantified mathematical form, let S ⊆ R^n, let G : R^n -> R^n, and
assume that G is differentiable at every point of S, relative to S. If
there are c ∈ R^n and rho > 0 such that
ball c rho ⊆ G '' S, then S has positive Lebesgue measure.
The proof uses the standard theorem, already in mathlib, that a differentiable
map from R^n to R^n sends every Lebesgue-null set to a Lebesgue-null set.
A quantitative image-measure lower bound.
In quantified mathematical form, let S ⊆ R^n, let G : R^n -> R^n, and
let M ∈ [0,∞] satisfy M ≠ 0 and M ≠ ∞. If ball c rho ⊆ G '' S and
volume (G '' S) ≤ M * volume S, then
volume (ball c rho) / M ≤ volume S.
A positive-measure consequence of the quantitative image-measure lower bound.
In quantified mathematical form, under the hypotheses of
volume_ball_div_le_of_ball_subset_image_of_image_le_mul, if rho > 0, then
S has positive Lebesgue measure.
A quantitative lower bound from the Jacobian image-measure estimate.
In quantified mathematical form, let S ⊆ R^n, let G : R^n -> R^n, and
let G' x be the Fréchet derivative of G at x relative to S for every
x ∈ S. Suppose S is measurable, ball c rho ⊆ G '' S, and
ofReal |det (G' x)| ≤ M for every x ∈ S, where M ≠ 0 and M ≠ ∞.
Then volume (ball c rho) / M ≤ volume S.
Quantitative closed-ball global contact-set lower bound with an explicit boundary-gap radius.
In quantified mathematical form, assume every boundary point of
closedBall x0 r satisfies f x ≤ f x0 - gamma, with gamma > 0. Let
rho = min (delta / 2) (gamma / (2 * ((n : Real) * r + 1))). If the
closed-ball global contact set is measurable, if z ↦ -G z has derivative
G' z at every point of this contact set relative to the contact set, and if
ofReal |det (G' z)| ≤ M on the contact set, where M ≠ 0 and M ≠ ∞, then
volume (ball 0 rho) / M ≤ volume (JensenGlobalContactSet f x0 r delta).
Uniform convergence preserves a positive boundary gap after discarding finitely many terms.
In quantified mathematical form, assume every boundary point of
closedBall x0 r satisfies f x ≤ f x0 - gamma, with gamma > 0, and assume
f_m -> f uniformly on closedBall x0 r. Then there exists N such that
for every m ≥ N and every boundary point x,
f_m x ≤ f_m x0 - gamma / 2.
A positive-measure consequence of the Jacobian image-measure estimate.
In quantified mathematical form, under the hypotheses of
volume_ball_div_le_of_ball_subset_image_of_hasFDerivWithinAt_det_le, if
rho > 0, then S has positive Lebesgue measure.
Measure lower bounds pass from a sequence of sets to its limsup.
In quantified mathematical form, let E m be a sequence of measurable
subsets of a measure space, and suppose all E m are contained in a set B
with finite measure. If a set K contains
⋂ n, ⋃ m, ⋃ (_ : n ≤ m), E m,
Positive measure passes from a sequence of uniformly positive measurable sets to any set containing their limsup.
In quantified mathematical form, under the hypotheses of
measure_limsup_le_of_forall_measure_le, if 0 < c, then 0 < μ K.
The limsup measure passage specialized to Jensen contact sets.
In quantified mathematical form, let f_m : R^n -> R be a sequence of
functions and let f : R^n -> R. Suppose there exists c > 0 such that, for
every natural number m, the set JensenContactSet (f_m) x0 r delta is
measurable and has Lebesgue measure at least c. If
⋂ n, ⋃ m, ⋃ (_ : n ≤ m), JensenContactSet (f_m) x0 r delta
is contained in JensenContactSet f x0 r delta, then
JensenContactSet f x0 r delta has positive Lebesgue measure.
Positive measure of the Jensen contact set from differentiability of the gradient image map.
In quantified mathematical form, assume the hypotheses which give contact
points for all sufficiently small linear perturbations, and assume that
f is differentiable on ball x0 r with gradient G. If the map
z ↦ -G z is differentiable at every point of
JensenContactSet f x0 r delta, relative to that contact set, then
JensenContactSet f x0 r delta has positive Lebesgue measure.
Quantitative Jensen contact-set lower bound from a determinant bound for the negative-gradient map.
In quantified mathematical form, assume the hypotheses which give contact
points for all sufficiently small linear perturbations, and let G be the
gradient of f on ball x0 r. Suppose that JensenContactSet f x0 r delta
is measurable, that z ↦ -G z has derivative G' z at every contact point
relative to the contact set, and that
ofReal |det (G' z)| ≤ M at every contact point, where M ≠ 0 and
M ≠ ∞. Then there exists rho > 0 such that
volume (ball 0 rho) / M ≤ volume (JensenContactSet f x0 r delta).
Quantitative Jensen lower bound for the closed-ball global contact set from a determinant bound for the negative-gradient map.
In quantified mathematical form, assume the hypotheses which give closed-ball
maximizers for all sufficiently small linear perturbations, and let G be the
gradient of f on ball x0 r. Suppose that
JensenGlobalContactSet f x0 r delta is measurable, that z ↦ -G z has
derivative G' z at every global contact point relative to the global contact
set, and that ofReal |det (G' z)| ≤ M at every global contact point, where
M ≠ 0 and M ≠ ∞. Then there exists rho > 0 such that
volume (ball 0 rho) / M ≤ volume (JensenGlobalContactSet f x0 r delta).
Quantitative Jensen lower bound for the closed-ball global contact set when the gradient is continuous.
In quantified mathematical form, under the smooth hypotheses used in Jensen's
lemma, suppose Df = G on ball x0 r, the map G is continuous, the map
z ↦ -G z has derivative G' z at every global contact point relative to
the global contact set, and ofReal |det (G' z)| ≤ M on the global contact
set, where M ≠ 0 and M ≠ ∞. Then there exists rho > 0 such that
volume (ball 0 rho) / M ≤ volume (JensenGlobalContactSet f x0 r delta).