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

Jensen Contact-Set Theorem (ContactSets)

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.

def ViscositySolns.JensenContactSet {n : ℕ} (f : Point n → ℝ) (x0 : Point n) (r delta : ℝ) : Set (Point n)

The contact set appearing in Jensen's lemma.

In quantified mathematical form, JensenContactSet f x0 r delta is the set of points x in the closed ball B(x0, r) for which there exists p ∈ B(0, delta) such that y ↦ f y + p · y has a local maximum at x.

Equations

• ViscositySolns.JensenContactSet f x0 r delta = {x : ViscositySolns.Point n | x ∈ Metric.closedBall x0 r ∧ ∃ p ∈ Metric.ball 0 delta, IsLocalMax (ViscositySolns.linearPerturbation f p) x}

def ViscositySolns.JensenGlobalContactSet {n : ℕ} (f : Point n → ℝ) (x0 : Point n) (r delta : ℝ) : Set (Point n)

The closed-ball global contact set appearing before the passage to local contacts in the proof of Jensen's lemma.

In quantified mathematical form, JensenGlobalContactSet f x0 r delta is the set of points x in the open ball B(x0, r) for which there exists p ∈ B(0, delta) such that x is a maximum point of y ↦ f y + p · y on the closed ball closedBall x0 r.

Equations

• One or more equations did not get rendered due to their size.

def ViscositySolns.JensenGradientGlobalContactSet {n : ℕ} (f : Point n → ℝ) (G : Point n → Point n) (x0 : Point n) (r delta : ℝ) : Set (Point n)

The closed-ball global contact set parametrized by the gradient.

In quantified mathematical form, JensenGradientGlobalContactSet f G x0 r δ is the set of all x ∈ ball x0 r such that -G x ∈ ball 0 δ and x maximizes y ↦ f y - G x · y on closedBall x0 r.

Equations

• One or more equations did not get rendered due to their size.

theorem ViscositySolns.measurableSet_jensenGradientGlobalContactSet {n : ℕ} {f : Point n → ℝ} {G : Point n → Point n} {x0 : Point n} {r delta : ℝ} (hf : Continuous f) (hG : Continuous G) : MeasurableSet (JensenGradientGlobalContactSet f G x0 r delta)

The gradient-parametrized global contact set is measurable when both the function and the gradient are continuous.

theorem ViscositySolns.JensenGlobalContactSet_eq_jensenGradientGlobalContactSet {n : ℕ} {f : Point n → ℝ} {G : Point n → Point n} {x0 : Point n} {r delta : ℝ} (hderiv : ∀ z ∈ Metric.ball x0 r, HasFDerivAt f (gradientLinearMap (G z)) z) : JensenGlobalContactSet f x0 r delta = JensenGradientGlobalContactSet f G x0 r delta

For a differentiable function, the closed-ball global contact set is the same as the gradient-parametrized global contact set.

In quantified mathematical form, if Df(x) = G x for every x ∈ ball x0 r, then an interior maximizer of y ↦ f y + p · y on closedBall x0 r satisfies p = -G x. Consequently the existential perturbation in JensenGlobalContactSet may be replaced by the single perturbation -G x.

theorem ViscositySolns.measurableSet_jensenGlobalContactSet_of_continuous_gradient {n : ℕ} {f : Point n → ℝ} {G : Point n → Point n} {x0 : Point n} {r delta : ℝ} (hf : Continuous f) (hG : Continuous G) (hderiv : ∀ z ∈ Metric.ball x0 r, HasFDerivAt f (gradientLinearMap (G z)) z) : MeasurableSet (JensenGlobalContactSet f x0 r delta)

The closed-ball global contact set is measurable for a differentiable function with continuous gradient.

theorem ViscositySolns.JensenGlobalContactSet.subset_ball {n : ℕ} (f : Point n → ℝ) (x0 : Point n) (r delta : ℝ) : JensenGlobalContactSet f x0 r delta ⊆ Metric.ball x0 r

The closed-ball global contact set is contained in the open ball appearing in its definition.

theorem ViscositySolns.JensenGlobalContactSet.subset_closedBall {n : ℕ} (f : Point n → ℝ) (x0 : Point n) (r delta : ℝ) : JensenGlobalContactSet f x0 r delta ⊆ Metric.closedBall x0 r

The closed-ball global contact set is contained in the closed ball with the same center and radius.

theorem ViscositySolns.JensenContactSet.subset_closedBall {n : ℕ} (f : Point n → ℝ) (x0 : Point n) (r delta : ℝ) : JensenContactSet f x0 r delta ⊆ Metric.closedBall x0 r

The contact set is contained in the closed ball appearing in its definition.

theorem ViscositySolns.JensenContactSet.mono_radius {n : ℕ} {f : Point n → ℝ} {x0 : Point n} {r₁ r₂ delta : ℝ} (hr : r₁ ≤ r₂) : JensenContactSet f x0 r₁ delta ⊆ JensenContactSet f x0 r₂ delta

The contact set is monotone in the radius of the closed ball.

In quantified mathematical form, if r₁ ≤ r₂, then every contact point in closedBall x0 r₁ is also a contact point in closedBall x0 r₂, with the same perturbing vector.

theorem ViscositySolns.JensenContactSet.measure_pos_of_mono_radius {n : ℕ} {f : Point n → ℝ} {x0 : Point n} {r₁ r₂ delta : ℝ} (hr : r₁ ≤ r₂) (hpos : 0 < MeasureTheory.volume (JensenContactSet f x0 r₁ delta)) : 0 < MeasureTheory.volume (JensenContactSet f x0 r₂ delta)

Positive measure of the contact set is preserved when the radius is enlarged.

In quantified mathematical form, if r₁ ≤ r₂ and JensenContactSet f x0 r₁ δ has positive Lebesgue measure, then JensenContactSet f x0 r₂ δ also has positive Lebesgue measure.

theorem ViscositySolns.JensenContactSet.mono_delta {n : ℕ} {f : Point n → ℝ} {x0 : Point n} {r delta₁ delta₂ : ℝ} (hdelta : delta₁ ≤ delta₂) : JensenContactSet f x0 r delta₁ ⊆ JensenContactSet f x0 r delta₂

The contact set is monotone in the allowed size of the perturbing vector.

In quantified mathematical form, if δ₁ ≤ δ₂, then every point obtained using a perturbing vector p ∈ ball 0 δ₁ is also obtained using a perturbing vector p ∈ ball 0 δ₂.

theorem ViscositySolns.JensenContactSet.measure_pos_of_mono_delta {n : ℕ} {f : Point n → ℝ} {x0 : Point n} {r delta₁ delta₂ : ℝ} (hdelta : delta₁ ≤ delta₂) (hpos : 0 < MeasureTheory.volume (JensenContactSet f x0 r delta₁)) : 0 < MeasureTheory.volume (JensenContactSet f x0 r delta₂)

Positive measure of the contact set is preserved when the allowed perturbing vectors are enlarged.

In quantified mathematical form, if δ₁ ≤ δ₂ and JensenContactSet f x0 r δ₁ has positive Lebesgue measure, then JensenContactSet f x0 r δ₂ also has positive Lebesgue measure.

theorem ViscositySolns.StrictLocalMax.mem_jensenContactSet {n : ℕ} {f : Point n → ℝ} {x0 : Point n} {r delta : ℝ} (h : StrictLocalMax f x0) (hr : 0 ≤ r) (hdelta : 0 < delta) : x0 ∈ JensenContactSet f x0 r delta

The strict maximum point belongs to the contact set for the zero perturbation.

In quantified mathematical form, if 0 ≤ r, 0 < δ, and x0 is a strict local maximum point of f, then x0 ∈ JensenContactSet f x0 r δ.

theorem ViscositySolns.abs_dotProduct_sub_dotProduct_center_le_of_mem_closedBall {n : ℕ} {x x0 p : Point n} {r : ℝ} (hx : x ∈ Metric.closedBall x0 r) : |p ⬝ᵥ x - p ⬝ᵥ x0| ≤ ↑n * ‖p‖ * r

The linear part of a perturbation is uniformly bounded on a closed ball.

In quantified mathematical form, if x ∈ closedBall x0 r, then

|p · x - p · x0| ≤ n ‖p‖ r,

where n is the dimension of R^n and the norm is the finite product norm used by Lean on Fin n -> Real.

theorem ViscositySolns.linearPerturbation_lt_center_of_boundary_gap {n : ℕ} {f : Point n → ℝ} {x x0 p : Point n} {r gamma : ℝ} (hx : x ∈ Metric.closedBall x0 r) (hboundary : dist x x0 = r) (hgap : ∀ y ∈ Metric.closedBall x0 r, dist y x0 = r → f y ≤ f x0 - gamma) (hp : ↑n * ‖p‖ * r < gamma) : linearPerturbation f p x < linearPerturbation f p x0

Small linear perturbations remain below the center on the boundary of a closed ball when the unperturbed function has a positive boundary gap.

In quantified mathematical form, suppose that every x ∈ closedBall x0 r with dist x x0 = r satisfies f x ≤ f x0 - gamma, and suppose n ‖p‖ r < gamma. Then every such boundary point satisfies f x + p · x < f x0 + p · x0.

theorem ViscositySolns.isMaxOn_linearPerturbation_closedBall_mem_ball_of_boundary_gap {n : ℕ} {f : Point n → ℝ} {z x0 p : Point n} {r gamma : ℝ} (hr : 0 ≤ r) (hgap : ∀ y ∈ Metric.closedBall x0 r, dist y x0 = r → f y ≤ f x0 - gamma) (hp : ↑n * ‖p‖ * r < gamma) (hz : z ∈ Metric.closedBall x0 r) (hmax : IsMaxOn (linearPerturbation f p) (Metric.closedBall x0 r) z) : z ∈ Metric.ball x0 r

A maximum point of a sufficiently small linear perturbation on a closed ball is not on the boundary.

In quantified mathematical form, assume 0 ≤ r, every boundary point x of closedBall x0 r satisfies f x ≤ f x0 - gamma, and n ‖p‖ r < gamma. If z maximizes y ↦ f y + p · y on closedBall x0 r, then dist z x0 < r.

theorem ViscositySolns.exists_pos_boundary_gap_of_continuousOn_sphere {n : ℕ} {f : Point n → ℝ} {x0 : Point n} {r : ℝ} (hf : ContinuousOn f (Metric.sphere x0 r)) (hstrict : ∀ x ∈ Metric.closedBall x0 r, dist x x0 = r → f x < f x0) : ∃ (gamma : ℝ), 0 < gamma ∧ ∀ x ∈ Metric.closedBall x0 r, dist x x0 = r → f x ≤ f x0 - gamma

Continuity and strict boundary inequality give a positive boundary gap.

In quantified mathematical form, suppose f is continuous on sphere x0 r, and suppose that every point x ∈ closedBall x0 r with dist x x0 = r satisfies f x < f x0. Then there exists gamma > 0 such that every such boundary point satisfies f x ≤ f x0 - gamma.

theorem ViscositySolns.exists_pos_boundary_gap_of_coordinateSemiconvexOn_larger_closedBall {n : ℕ} {f : Point n → ℝ} {x0 : Point n} {r R lambda : ℝ} (hsemi : CoordinateSemiconvexOn lambda (Metric.closedBall x0 R) f) (hrR : r < R) (hstrict : ∀ x ∈ Metric.closedBall x0 r, dist x x0 = r → f x < f x0) : ∃ (gamma : ℝ), 0 < gamma ∧ ∀ x ∈ Metric.closedBall x0 r, dist x x0 = r → f x ≤ f x0 - gamma

Semiconvexity on a larger closed ball and strict boundary inequality on a smaller closed ball give a positive boundary gap.

In quantified mathematical form, suppose r < R, f : R^n -> R satisfies the coordinate semiconvexity inequality on closedBall x0 R, and every x ∈ closedBall x0 r with dist x x0 = r satisfies f x < f x0. Then there exists gamma > 0 such that every such boundary point satisfies f x ≤ f x0 - gamma.

theorem ViscositySolns.exists_pos_boundary_gap_eventually_isMaxOn_mem_ball {n : ℕ} {f : Point n → ℝ} {x0 : Point n} {r : ℝ} (hr : 0 ≤ r) (hf : ContinuousOn f (Metric.sphere x0 r)) (hstrict : ∀ x ∈ Metric.closedBall x0 r, dist x x0 = r → f x < f x0) : ∃ (gamma : ℝ), 0 < gamma ∧ ∀ (p z : Point n), ↑n * ‖p‖ * r < gamma → z ∈ Metric.closedBall x0 r → IsMaxOn (linearPerturbation f p) (Metric.closedBall x0 r) z → z ∈ Metric.ball x0 r

The boundary-exclusion theorem with the positive boundary gap supplied by continuity and strict boundary inequality.

In quantified mathematical form, suppose f is continuous on sphere x0 r and f x < f x0 for every boundary point of closedBall x0 r. Then there exists gamma > 0 such that every perturbing vector p satisfying n ‖p‖ r < gamma has the following property: every maximum of x ↦ f x + p · x on closedBall x0 r lies in ball x0 r.

theorem ViscositySolns.mem_jensenContactSet_of_isMaxOn_closedBall_of_mem_ball {n : ℕ} {f : Point n → ℝ} {z x0 p : Point n} {r delta : ℝ} (hzClosed : z ∈ Metric.closedBall x0 r) (hzBall : z ∈ Metric.ball x0 r) (hpDelta : p ∈ Metric.ball 0 delta) (hmax : IsMaxOn (linearPerturbation f p) (Metric.closedBall x0 r) z) : z ∈ JensenContactSet f x0 r delta

An interior maximum on the closed ball gives a point of Jensen's contact set.

In quantified mathematical form, if z maximizes y ↦ f y + p · y on closedBall x0 r, if z ∈ ball x0 r, and if p ∈ ball 0 δ, then z ∈ JensenContactSet f x0 r δ.

theorem ViscositySolns.JensenGlobalContactSet.subset_jensenContactSet {n : ℕ} (f : Point n → ℝ) (x0 : Point n) (r delta : ℝ) : JensenGlobalContactSet f x0 r delta ⊆ JensenContactSet f x0 r delta

Every closed-ball global contact point is a Jensen contact point.

In quantified mathematical form, if x ∈ B(x0, r) and there exists p ∈ B(0, delta) such that x maximizes y ↦ f y + p · y on closedBall x0 r, then x ∈ JensenContactSet f x0 r delta.

theorem ViscositySolns.tendsto_eval_of_uniformOn_closedBall_comp {n : ℕ} {fseq : ℕ → Point n → ℝ} {f : Point n → ℝ} {x0 y : Point n} {r : ℝ} {idx : ℕ → ℕ} (hunif : ∀ (eps : ℝ), 0 < eps → ∃ (N : ℕ), ∀ (m : ℕ), N ≤ m → ∀ z ∈ Metric.closedBall x0 r, |fseq m z - f z| ≤ eps) (hidx : Filter.Tendsto idx Filter.atTop Filter.atTop) (hy : y ∈ Metric.closedBall x0 r) : Filter.Tendsto (fun (j : ℕ) => fseq (idx j) y) Filter.atTop (nhds (f y))

Uniform convergence on a closed ball gives convergence at each point of that closed ball after passing to any sequence of indices tending to infinity.

In quantified mathematical form, assume that for every ε > 0 there exists N such that, for every m ≥ N and every y ∈ closedBall x0 r, |f_m(y) - f(y)| ≤ ε. If i_j -> ∞ and y ∈ closedBall x0 r, then f_{i_j}(y) -> f(y).

theorem ViscositySolns.JensenGlobalContactSet.limsup_subset_jensenContactSet_of_uniformOn_closedBall {n : ℕ} {fseq : ℕ → Point n → ℝ} {f : Point n → ℝ} {x0 : Point n} {r delta : ℝ} (hdelta : 0 < delta) (hunif : ∀ (eps : ℝ), 0 < eps → ∃ (N : ℕ), ∀ (m : ℕ), N ≤ m → ∀ z ∈ Metric.closedBall x0 r, |fseq m z - f z| ≤ eps) : ⋂ (k : ℕ), ⋃ (m : ℕ), ⋃ (_ : k ≤ m), JensenGlobalContactSet (fseq m) x0 r (delta / 2) ⊆ JensenContactSet f x0 r delta

Set-theoretic limsup containment for closed-ball global contact sets under uniform convergence on the closed ball.

In quantified mathematical form, assume that, for every ε > 0, there exists N such that, for every m ≥ N and every y ∈ closedBall x0 r, |f_m(y) - f(y)| ≤ ε. If δ > 0, then every point which belongs to

⋂ k, ⋃ m, ⋃ (_ : k ≤ m), JensenGlobalContactSet f_m x0 r (δ / 2)

belongs to JensenContactSet f x0 r δ.

theorem ViscositySolns.exists_mem_jensenContactSet_of_boundary_gap {n : ℕ} {f : Point n → ℝ} {x0 p : Point n} {r gamma delta : ℝ} (hr : 0 ≤ r) (hf : ContinuousOn f (Metric.closedBall x0 r)) (hgap : ∀ y ∈ Metric.closedBall x0 r, dist y x0 = r → f y ≤ f x0 - gamma) (hpSmall : ↑n * ‖p‖ * r < gamma) (hpDelta : p ∈ Metric.ball 0 delta) : ∃ z ∈ JensenContactSet f x0 r delta, IsMaxOn (linearPerturbation f p) (Metric.closedBall x0 r) z ∧ z ∈ Metric.ball x0 r

Under a positive boundary gap, every sufficiently small perturbing vector produces a point of Jensen's contact set.

In quantified mathematical form, assume 0 ≤ r, f is continuous on closedBall x0 r, every boundary point satisfies f x ≤ f x0 - gamma, p ∈ ball 0 δ, and n ‖p‖ r < gamma. Then there exists z ∈ JensenContactSet f x0 r δ such that z maximizes y ↦ f y + p · y on closedBall x0 r, and z ∈ ball x0 r.

theorem ViscositySolns.exists_pos_boundary_gap_forall_small_perturbation_exists_contact {n : ℕ} {f : Point n → ℝ} {x0 : Point n} {r : ℝ} (hr : 0 ≤ r) (hfClosed : ContinuousOn f (Metric.closedBall x0 r)) (hfSphere : ContinuousOn f (Metric.sphere x0 r)) (hstrict : ∀ x ∈ Metric.closedBall x0 r, dist x x0 = r → f x < f x0) : ∃ (gamma : ℝ), 0 < gamma ∧ ∀ {delta : ℝ}, ∀ p ∈ Metric.ball 0 delta, ↑n * ‖p‖ * r < gamma → ∃ z ∈ JensenContactSet f x0 r delta, IsMaxOn (linearPerturbation f p) (Metric.closedBall x0 r) z ∧ z ∈ Metric.ball x0 r

The preceding contact-point existence theorem with the positive boundary gap supplied by compactness.

In quantified mathematical form, assume f is continuous on closedBall x0 r and on sphere x0 r, and assume f x < f x0 for every boundary point. Then there exists gamma > 0 such that every p ∈ ball 0 δ satisfying n ‖p‖ r < gamma produces a point of JensenContactSet f x0 r δ which maximizes the corresponding linear perturbation on closedBall x0 r and lies in ball x0 r.

theorem ViscositySolns.exists_pos_boundary_gap_forall_small_perturbation_exists_contact_gradient {n : ℕ} {f : Point n → ℝ} {x0 : Point n} {r : ℝ} {G : Point n → Point n} (hr : 0 ≤ r) (hfClosed : ContinuousOn f (Metric.closedBall x0 r)) (hfSphere : ContinuousOn f (Metric.sphere x0 r)) (hstrict : ∀ x ∈ Metric.closedBall x0 r, dist x x0 = r → f x < f x0) (hderiv : ∀ z ∈ Metric.ball x0 r, HasFDerivAt f (gradientLinearMap (G z)) z) : ∃ (gamma : ℝ), 0 < gamma ∧ ∀ {delta : ℝ}, ∀ q ∈ Metric.ball 0 delta, ↑n * ‖q‖ * r < gamma → ∃ z ∈ JensenContactSet f x0 r delta, IsMaxOn (linearPerturbation f q) (Metric.closedBall x0 r) z ∧ z ∈ Metric.ball x0 r ∧ G z + q = 0

The compact contact-point selection theorem together with first-order calculus.

In quantified mathematical form, assume f is continuous on closedBall x0 r and on sphere x0 r, and assume f x < f x0 for every boundary point. Let G : R^n -> R^n be a function such that, for every z ∈ ball x0 r, f is differentiable at z with gradient G z. Then there exists gamma > 0 such that, for every delta and every vector q, if q ∈ ball 0 delta and n ‖q‖ r < gamma, then there exists z such that

• z ∈ JensenContactSet f x0 r delta;
• z maximizes y ↦ f y + q · y on closedBall x0 r;
• z ∈ ball x0 r;
• G z + q = 0.