Ported for Lean Pool: imports relocated and code adapted to Lean/Mathlib v4.34.0.

Jensen Contact-Set Theorem (ContDiffHessian)

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.

theorem ViscositySolns.hasFDerivAt_coordinate_gradient_fderiv {n : ℕ} {f : Point n → ℝ} (hf : ContDiff ℝ 2 f) (x : Point n) : HasFDerivAt (fun (y : Point n) => linearMapGradient (fderiv ℝ f y)) (linearMapGradientCLM ∘SL fderiv ℝ (fderiv ℝ f) x) x

Derivative of the coordinate gradient map of a C^2 function.

In quantified mathematical form, if f : R^n -> R is twice continuously differentiable, then the Fréchet derivative at x of y ↦ linearMapGradient (fderiv Real f y) is obtained by composing the second Fréchet derivative of f at x with the coordinate-gradient map.

theorem ViscositySolns.hasFDerivAt_neg_coordinate_gradient_fderiv {n : ℕ} {f : Point n → ℝ} (hf : ContDiff ℝ 2 f) (x : Point n) : HasFDerivAt (fun (y : Point n) => -linearMapGradient (fderiv ℝ f y)) (-linearMapGradientCLM ∘SL fderiv ℝ (fderiv ℝ f) x) x

Derivative of the negative coordinate gradient map of a C^2 function.

theorem ViscositySolns.toMatrix_coordinateGradient_comp {n : ℕ} (D2 : Point n →L[ℝ] Point n →L[ℝ] ℝ) : LinearMap.toMatrix' ↑(linearMapGradientCLM ∘SL D2) = Matrix.transpose (bilinearMapHessian D2)

The matrix of the derivative of the coordinate-gradient map is the transpose of the coordinate Hessian represented by the second Fréchet derivative.

theorem ViscositySolns.abs_det_neg_coordinateGradient_comp {n : ℕ} (D2 : Point n →L[ℝ] Point n →L[ℝ] ℝ) : |(-linearMapGradientCLM ∘SL D2).det| = |Matrix.det (bilinearMapHessian D2)|

The absolute determinant of the derivative of the negative coordinate-gradient map equals the absolute determinant of the coordinate Hessian represented by the second Fréchet derivative.

theorem ViscositySolns.exists_pos_radius_volume_ball_div_le_jensenGlobalContactSet_of_contDiff_two_neg_gradient_det_le {n : ℕ} {f : Point n → ℝ} {x0 : Point n} {r delta : ℝ} {M : ENNReal} (hr : 0 ≤ r) (hdelta : 0 < delta) (hf : ContDiff ℝ 2 f) (hstrict : ∀ x ∈ Metric.closedBall x0 r, dist x x0 = r → f x < f x0) (hM0 : M ≠ 0) (hMtop : M ≠ ⊤) (hdet : ∀ z ∈ JensenGlobalContactSet f x0 r delta, ENNReal.ofReal |(-linearMapGradientCLM ∘SL fderiv ℝ (fderiv ℝ f) z).det| ≤ M) : ∃ (rho : ℝ), 0 < rho ∧ MeasureTheory.volume (Metric.ball 0 rho) / M ≤ MeasureTheory.volume (JensenGlobalContactSet f x0 r delta)

Quantitative Jensen lower bound for the closed-ball global contact set of a C^2 function, stated with the determinant bound for the derivative of the negative gradient map as the remaining pointwise hypothesis.

In quantified mathematical form, assume f : R^n -> R is twice continuously differentiable, delta > 0, and every boundary point of closedBall x0 r has strictly smaller f-value than x0. If the determinant of the derivative of z ↦ -Df(z) is bounded above by M on the closed-ball 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).

theorem ViscositySolns.exists_pos_radius_volume_ball_div_le_jensenGlobalContactSet_of_contDiff_two_hessian_det_le {n : ℕ} {f : Point n → ℝ} {x0 : Point n} {r delta : ℝ} {M : ENNReal} (hr : 0 ≤ r) (hdelta : 0 < delta) (hf : ContDiff ℝ 2 f) (hstrict : ∀ x ∈ Metric.closedBall x0 r, dist x x0 = r → f x < f x0) (hM0 : M ≠ 0) (hMtop : M ≠ ⊤) (hdet : ∀ z ∈ JensenGlobalContactSet f x0 r delta, ENNReal.ofReal |Matrix.det (bilinearMapHessian (fderiv ℝ (fderiv ℝ f) z))| ≤ M) : ∃ (rho : ℝ), 0 < rho ∧ MeasureTheory.volume (Metric.ball 0 rho) / M ≤ MeasureTheory.volume (JensenGlobalContactSet f x0 r delta)

Quantitative Jensen lower bound for the closed-ball global contact set of a C^2 function, stated with the determinant bound for the coordinate Hessian.

In quantified mathematical form, assume f : R^n -> R is twice continuously differentiable, delta > 0, and every boundary point of closedBall x0 r has strictly smaller f-value than x0. If the determinant of the coordinate Hessian represented by the second Fréchet derivative is bounded above by M on the closed-ball 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).

theorem ViscositySolns.hasSecondOrderJet_of_contDiff_two {n : ℕ} {f : Point n → ℝ} (hf : ContDiff ℝ 2 f) (x : Point n) : HasSecondOrderJet f x (linearMapGradient (fderiv ℝ f x)) (bilinearMapHessian (fderiv ℝ (fderiv ℝ f) x))

A C^2 function has the ordinary two-sided second-order jet determined by its first and second Fréchet derivatives.

theorem ViscositySolns.hessian_le_zero_of_mem_jensenGlobalContactSet_contDiff_two {n : ℕ} {f : Point n → ℝ} {x x0 : Point n} {r delta : ℝ} (hf : ContDiff ℝ 2 f) (hHerm : Matrix.IsHermitian (bilinearMapHessian (fderiv ℝ (fderiv ℝ f) x))) (hx : x ∈ JensenGlobalContactSet f x0 r delta) : bilinearMapHessian (fderiv ℝ (fderiv ℝ f) x) ≤ 0

At a closed-ball global contact point of a C^2 function, the coordinate Hessian is nonpositive.

In quantified mathematical form, if x is an interior point of closedBall x0 r where y ↦ f y + p · y attains its maximum on the closed ball, then D^2 f(x) ≤ 0.

theorem ViscositySolns.contDiff_two_bilinearMapHessian_isHermitian {n : ℕ} {f : Point n → ℝ} (hf : ContDiff ℝ 2 f) (x : Point n) : Matrix.IsHermitian (bilinearMapHessian (fderiv ℝ (fderiv ℝ f) x))

The coordinate Hessian of a C^2 real-valued function is Hermitian.

In quantified mathematical form, if f : R^n -> R is twice continuously differentiable, then for every x : R^n and all coordinate vectors e_i, e_j, the equality D^2 f(x)(e_i, e_j) = D^2 f(x)(e_j, e_i) holds.

theorem ViscositySolns.hessian_lower_bound_of_convexOn_semiconvexConvexification_contDiff_two {n : ℕ} {f : Point n → ℝ} {lambda : ℝ} (hf : ContDiff ℝ 2 f) (hconv : ConvexOn ℝ Set.univ (semiconvexConvexification lambda f)) (x : Point n) : -(lambda • 1) ≤ bilinearMapHessian (fderiv ℝ (fderiv ℝ f) x)

Convexity of the semiconvex convexification gives the lower Hessian bound for a C^2 function.

In quantified mathematical form, if f : R^n -> R is twice continuously differentiable and x ↦ f x + (lambda / 2) |x|^2 is convex on R^n, then for every x : R^n,

-lambda I ≤ D^2 f(x).

theorem ViscositySolns.hessian_lower_bound_of_convexOn_closedBall_semiconvexConvexification_contDiff_two {n : ℕ} {f : Point n → ℝ} {x x0 : Point n} {r lambda : ℝ} (hf : ContDiff ℝ 2 f) (hconv : ConvexOn ℝ (Metric.closedBall x0 r) (semiconvexConvexification lambda f)) (hx : x ∈ Metric.ball x0 r) : -(lambda • 1) ≤ bilinearMapHessian (fderiv ℝ (fderiv ℝ f) x)

Convexity of the semiconvex convexification on a closed ball gives the lower Hessian bound for a C^2 function at interior points of that ball.

In quantified mathematical form, if f : R^n -> R is twice continuously differentiable, x ∈ ball x0 r, and y ↦ f y + (lambda / 2) |y|^2 is convex on closedBall x0 r, then

-lambda I ≤ D^2 f(x).

theorem ViscositySolns.exists_pos_radius_volume_ball_div_le_jensenGlobalContactSet_of_contDiff_two_hessian_bounds {n : ℕ} {f : Point n → ℝ} {x0 : Point n} {r delta lambda : ℝ} (hr : 0 ≤ r) (hdelta : 0 < delta) (hf : ContDiff ℝ 2 f) (hstrict : ∀ x ∈ Metric.closedBall x0 r, dist x x0 = r → f x < f x0) (hlambda : 0 ≤ lambda) (hHerm : ∀ z ∈ JensenGlobalContactSet f x0 r delta, Matrix.IsHermitian (bilinearMapHessian (fderiv ℝ (fderiv ℝ f) z))) (hlower : ∀ z ∈ JensenGlobalContactSet f x0 r delta, -(lambda • 1) ≤ bilinearMapHessian (fderiv ℝ (fderiv ℝ f) z)) (hupper : ∀ z ∈ JensenGlobalContactSet f x0 r delta, bilinearMapHessian (fderiv ℝ (fderiv ℝ f) z) ≤ 0) : ∃ (rho : ℝ), 0 < rho ∧ MeasureTheory.volume (Metric.ball 0 rho) / ENNReal.ofReal (max (lambda ^ n) 1) ≤ MeasureTheory.volume (JensenGlobalContactSet f x0 r delta)

Quantitative Jensen lower bound for the closed-ball global contact set of a C^2 function from Hessian order bounds.

In quantified mathematical form, assume f : R^n -> R is twice continuously differentiable, delta > 0, and every boundary point of closedBall x0 r has strictly smaller f-value than x0. Suppose that, at every point of the closed-ball global contact set, the coordinate Hessian H z represented by the second Fréchet derivative is Hermitian and satisfies -lambda I ≤ H z ≤ 0, with 0 ≤ lambda. Then there exists rho > 0 such that

volume (ball 0 rho) / ofReal (max (lambda^n) 1) ≤ volume (JensenGlobalContactSet f x0 r delta).

theorem ViscositySolns.exists_pos_radius_volume_ball_div_le_jensenGlobalContactSet_of_contDiff_two_hessian_lower_bound {n : ℕ} {f : Point n → ℝ} {x0 : Point n} {r delta lambda : ℝ} (hr : 0 ≤ r) (hdelta : 0 < delta) (hf : ContDiff ℝ 2 f) (hstrict : ∀ x ∈ Metric.closedBall x0 r, dist x x0 = r → f x < f x0) (hlambda : 0 ≤ lambda) (hHerm : ∀ z ∈ JensenGlobalContactSet f x0 r delta, Matrix.IsHermitian (bilinearMapHessian (fderiv ℝ (fderiv ℝ f) z))) (hlower : ∀ z ∈ JensenGlobalContactSet f x0 r delta, -(lambda • 1) ≤ bilinearMapHessian (fderiv ℝ (fderiv ℝ f) z)) : ∃ (rho : ℝ), 0 < rho ∧ MeasureTheory.volume (Metric.ball 0 rho) / ENNReal.ofReal (max (lambda ^ n) 1) ≤ MeasureTheory.volume (JensenGlobalContactSet f x0 r delta)

Quantitative Jensen lower bound for the closed-ball global contact set of a C^2 function from the semiconvex lower Hessian bound.

In quantified mathematical form, assume f : R^n -> R is twice continuously differentiable, delta > 0, and every boundary point of closedBall x0 r has strictly smaller f-value than x0. Suppose that, at every point of the closed-ball global contact set, the coordinate Hessian is Hermitian and satisfies -lambda I ≤ D^2 f, with 0 ≤ lambda. Then there exists rho > 0 such that

volume (ball 0 rho) / ofReal (max (lambda^n) 1) ≤ volume (JensenGlobalContactSet f x0 r delta).

The upper Hessian inequality D^2 f ≤ 0 is supplied by the closed-ball maximum condition at each interior contact point.

theorem ViscositySolns.exists_pos_radius_volume_ball_div_le_jensenGlobalContactSet_of_hessian_lower_bound_no_hermitian {n : ℕ} {f : Point n → ℝ} {x0 : Point n} {r delta lambda : ℝ} (hr : 0 ≤ r) (hdelta : 0 < delta) (hf : ContDiff ℝ 2 f) (hstrict : ∀ x ∈ Metric.closedBall x0 r, dist x x0 = r → f x < f x0) (hlambda : 0 ≤ lambda) (hlower : ∀ z ∈ JensenGlobalContactSet f x0 r delta, -(lambda • 1) ≤ bilinearMapHessian (fderiv ℝ (fderiv ℝ f) z)) : ∃ (rho : ℝ), 0 < rho ∧ MeasureTheory.volume (Metric.ball 0 rho) / ENNReal.ofReal (max (lambda ^ n) 1) ≤ MeasureTheory.volume (JensenGlobalContactSet f x0 r delta)

Quantitative Jensen lower bound for the closed-ball global contact set of a C^2 function from a pointwise semiconvex Hessian lower bound.

In quantified mathematical form, assume f : R^n -> R is twice continuously differentiable, delta > 0, and every boundary point of closedBall x0 r has strictly smaller f-value than x0. If 0 ≤ lambda and -lambda I ≤ D^2 f(z) at every point z of the closed-ball global contact set, then there exists rho > 0 such that

volume (ball 0 rho) / ofReal (max (lambda^n) 1) ≤ volume (JensenGlobalContactSet f x0 r delta).

The Hermitian property of D^2 f follows from the symmetry of second derivatives for C^2 real-valued functions, and the upper inequality D^2 f ≤ 0 follows from the local-maximum second-derivative test.

theorem ViscositySolns.exists_pos_radius_volume_ball_div_le_jensenGlobalContactSet_of_contDiff_two_convexified {n : ℕ} {f : Point n → ℝ} {x0 : Point n} {r delta lambda : ℝ} (hr : 0 ≤ r) (hdelta : 0 < delta) (hf : ContDiff ℝ 2 f) (hstrict : ∀ x ∈ Metric.closedBall x0 r, dist x x0 = r → f x < f x0) (hlambda : 0 ≤ lambda) (hconv : ConvexOn ℝ Set.univ (semiconvexConvexification lambda f)) : ∃ (rho : ℝ), 0 < rho ∧ MeasureTheory.volume (Metric.ball 0 rho) / ENNReal.ofReal (max (lambda ^ n) 1) ≤ MeasureTheory.volume (JensenGlobalContactSet f x0 r delta)

Quantitative Jensen lower bound for the closed-ball global contact set of a smooth semiconvex function.

In quantified mathematical form, assume f : R^n -> R is twice continuously differentiable, 0 ≤ lambda, delta > 0, every boundary point of closedBall x0 r has strictly smaller f-value than x0, and x ↦ f x + (lambda / 2) |x|^2 is convex on R^n. Then there exists rho > 0 such that

volume (ball 0 rho) / ofReal (max (lambda^n) 1) ≤ volume (JensenGlobalContactSet f x0 r delta).

theorem ViscositySolns.volume_explicit_ball_div_le_jensenGlobalContactSet_of_contDiff_two_convexified_boundary_gap {n : ℕ} {f : Point n → ℝ} {x0 : Point n} {r delta gamma lambda : ℝ} (hr : 0 ≤ r) (hdelta : 0 < delta) (hgamma : 0 < gamma) (hf : ContDiff ℝ 2 f) (hgap : ∀ y ∈ Metric.closedBall x0 r, dist y x0 = r → f y ≤ f x0 - gamma) (hlambda : 0 ≤ lambda) (hconv : ConvexOn ℝ (Metric.closedBall x0 r) (semiconvexConvexification lambda f)) : MeasureTheory.volume (Metric.ball 0 (min (delta / 2) (gamma / (2 * (↑n * r + 1))))) / ENNReal.ofReal (max (lambda ^ n) 1) ≤ MeasureTheory.volume (JensenGlobalContactSet f x0 r delta)

Quantitative Jensen lower bound for a smooth semiconvex function, with the boundary-gap radius made explicit.

In quantified mathematical form, assume f : R^n -> R is twice continuously differentiable, 0 ≤ lambda, delta > 0, every boundary point of closedBall x0 r satisfies f x ≤ f x0 - gamma, with gamma > 0, and x ↦ f x + (lambda / 2) |x|^2 is convex on closedBall x0 r. Then

volume (ball 0 rho) / ofReal (max (lambda^n) 1) ≤ volume (JensenGlobalContactSet f x0 r delta),

where rho = min (delta / 2) (gamma / (2 * ((n : Real) * r + 1))).

theorem ViscositySolns.exists_tail_measurable_common_lower_bound_jensenGlobalContactSet_of_uniformOn_convexified {n : ℕ} {f : Point n → ℝ} {fseq : ℕ → Point n → ℝ} {x0 : Point n} {r delta gamma lambda : ℝ} (hr : 0 ≤ r) (hdelta : 0 < delta) (hgamma : 0 < gamma) (hgap : ∀ x ∈ Metric.closedBall x0 r, dist x x0 = r → f x ≤ f x0 - gamma) (hunif : ∀ (eps : ℝ), 0 < eps → ∃ (N : ℕ), ∀ (m : ℕ), N ≤ m → ∀ z ∈ Metric.closedBall x0 r, |fseq m z - f z| ≤ eps) (hfseq : ∀ (m : ℕ), ContDiff ℝ 2 (fseq m)) (hlambda : 0 ≤ lambda) (hconvseq : ∀ (m : ℕ), ConvexOn ℝ (Metric.closedBall x0 r) (semiconvexConvexification lambda (fseq m))) : ∃ (N : ℕ) (c : ENNReal), 0 < c ∧ (∀ (m : ℕ), N ≤ m → MeasurableSet (JensenGlobalContactSet (fseq m) x0 r delta)) ∧ ∀ (m : ℕ), N ≤ m → c ≤ MeasureTheory.volume (JensenGlobalContactSet (fseq m) x0 r delta)

Uniformly convergent smooth semiconvex approximants have a common lower measure bound for their closed-ball global contact sets 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. Suppose also that every f_m is twice continuously differentiable and that x ↦ f_m x + (lambda / 2) |x|^2 is convex on closedBall x0 r, with the same lambda ≥ 0 for all m. Then there are a natural number N and a number c > 0 such that, for every m ≥ N,

• JensenGlobalContactSet f_m x0 r delta is measurable;
• c ≤ volume (JensenGlobalContactSet f_m x0 r delta).

theorem ViscositySolns.volume_pos_jensenContactSet_of_contDiff_two {n : ℕ} {f : Point n → ℝ} {x0 : Point n} {r delta : ℝ} (hr : 0 ≤ r) (hdelta : 0 < delta) (hf : ContDiff ℝ 2 f) (hstrict : ∀ x ∈ Metric.closedBall x0 r, dist x x0 = r → f x < f x0) : 0 < MeasureTheory.volume (JensenContactSet f x0 r delta)

Positive measure of the Jensen contact set for a globally C^2 function.

In quantified mathematical form, if f : R^n -> R is twice continuously differentiable, if delta > 0, and if every point of closedBall x0 r whose distance from x0 is exactly r has strictly smaller f-value than x0, then JensenContactSet f x0 r delta has positive Lebesgue measure.

theorem ViscositySolns.volume_pos_jensenContactSet_of_contDiff_two_closedBall_strict {n : ℕ} {f : Point n → ℝ} {x0 : Point n} {r delta : ℝ} (hr : 0 < r) (hdelta : 0 < delta) (hf : ContDiff ℝ 2 f) (hstrict : ∀ x ∈ Metric.closedBall x0 r, x ≠ x0 → f x < f x0) : 0 < MeasureTheory.volume (JensenContactSet f x0 r delta)

Positive measure of the Jensen contact set for a globally C^2 function, using the strict maximum hypothesis on the whole closed ball.

In quantified mathematical form, if r > 0, delta > 0, f : R^n -> R is twice continuously differentiable, and f x < f x0 for every x ∈ closedBall x0 r with x ≠ x0, then JensenContactSet f x0 r delta has positive Lebesgue measure.