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

Sup-convolution declarations (SuperjetTransfer)

Part of the compact-set sup-convolution development used in the appendix proof of the maximum principle for semicontinuous functions. Split from SupConvolution.lean; see the umbrella module docstring.

noncomputable def ViscositySolns.supConvolutionKernel {n : ℕ} (lambda : ℝ) (u : Point n → ℝ) (ξ x : Point n) : ℝ

The function whose supremum defines the sup-convolution at ξ.

In standard mathematical notation this is

x ↦ u(x) - (λ / 2) ∑ i, (x_i - ξ_i)^2.

Equations

• ViscositySolns.supConvolutionKernel lambda u ξ x = u x - lambda / 2 * (x - ξ) ⬝ᵥ (x - ξ)

noncomputable def ViscositySolns.compactSupConvolution {n : ℕ} (lambda : ℝ) (K : Set (Point n)) (u : Point n → ℝ) (ξ : Point n) : ℝ

The compact-set sup-convolution value.

In standard mathematical notation this is

sup { u(x) - (λ / 2) ∑ i, (x_i - ξ_i)^2 | x ∈ K }.

This declaration is intended for compact nonempty K; the accompanying maximum-existence theorem supplies a point where the displayed supremum is attained under upper semicontinuity.

Equations

• ViscositySolns.compactSupConvolution lambda K u ξ = sSup ((fun (x : ViscositySolns.Point n) => ViscositySolns.supConvolutionKernel lambda u ξ x) '' K)

theorem ViscositySolns.upperSemicontinuousOn_supConvolutionKernel {n : ℕ} {K : Set (Point n)} {u : Point n → ℝ} {lambda : ℝ} {ξ : Point n} (hu : UpperSemicontinuousOn u K) : UpperSemicontinuousOn (fun (x : Point n) => supConvolutionKernel lambda u ξ x) K

If u is upper semicontinuous on K, then the sup-convolution kernel is upper semicontinuous on K.

In quantified mathematical form, for every real number λ and point ξ, if u is upper semicontinuous on K, then x ↦ u x - (λ / 2) * ∑ i, (x i - ξ i)^2 is upper semicontinuous on K.

theorem ViscositySolns.exists_isMaxOn_supConvolutionKernel_of_isCompact {n : ℕ} {K : Set (Point n)} {u : Point n → ℝ} {lambda : ℝ} {ξ : Point n} (hKne : K.Nonempty) (hKcompact : IsCompact K) (hu : UpperSemicontinuousOn u K) : ∃ x ∈ K, IsMaxOn (fun (y : Point n) => supConvolutionKernel lambda u ξ y) K x

On a nonempty compact set, the sup-convolution kernel attains a maximum.

In quantified mathematical form, if K is nonempty and compact and u is upper semicontinuous on K, then for every λ and ξ there exists x ∈ K such that for every y ∈ K,

u y - (λ / 2) * ∑ i, (y i - ξ i)^2 ≤ u x - (λ / 2) * ∑ i, (x i - ξ i)^2.

theorem ViscositySolns.compactSupConvolution_eq_of_isMaxOn {n : ℕ} {K : Set (Point n)} {u : Point n → ℝ} {lambda : ℝ} {ξ y : Point n} (hy : y ∈ K) (hmax : IsMaxOn (fun (z : Point n) => supConvolutionKernel lambda u ξ z) K y) : compactSupConvolution lambda K u ξ = supConvolutionKernel lambda u ξ y

If the sup-convolution kernel has a maximum point y on K, then the compact sup-convolution is the kernel value at y.

In quantified mathematical form, if y ∈ K and for every z ∈ K,

u z - (lambda / 2) * ∑ i, (z i - ξ i)^2 ≤ u y - (lambda / 2) * ∑ i, (y i - ξ i)^2,

then

compactSupConvolution lambda K u ξ = u y - (lambda / 2) * ∑ i, (y i - ξ i)^2.

theorem ViscositySolns.supConvolutionKernel_le_compactSupConvolution_of_exists_isMaxOn {n : ℕ} {K : Set (Point n)} {u : Point n → ℝ} {lambda : ℝ} (hmax_exists : ∀ (ξ : Point n), ∃ y ∈ K, IsMaxOn (fun (z : Point n) => supConvolutionKernel lambda u ξ z) K y) {z ξ : Point n} (hz : z ∈ K) : supConvolutionKernel lambda u ξ z ≤ compactSupConvolution lambda K u ξ

If the sup-convolution kernel attains a maximum on K at every ξ, then each kernel value is bounded above by the compact sup-convolution value.

In quantified mathematical form, suppose that for every ξ there exists y ∈ K such that y is a maximum point on K of z ↦ u z - (lambda / 2) * ∑ i, (z i - ξ i)^2. Then for every z ∈ K and every ξ,

u z - (lambda / 2) * ∑ i, (z i - ξ i)^2 ≤ compactSupConvolution lambda K u ξ.

theorem ViscositySolns.superjet_of_superjet_supConvolutionMajorant {n : ℕ} {K : Set (Point n)} {v vhat : Point n → ℝ} {lambda : ℝ} {η y q : Point n} {Y : Hessian n} (hmajor : ∀ z ∈ K, ∀ (ξ : Point n), supConvolutionKernel lambda v ξ z ≤ vhat ξ) (hvalue : vhat η = supConvolutionKernel lambda v η y) (hJ : { gradient := q, hessian := Y } ∈ Superjet Set.univ vhat η) : { gradient := q, hessian := Y } ∈ Superjet K v y

The superjet transfer lemma for a function majorized by sup-convolution kernels.

In quantified mathematical form, let vhat : Point n -> Real be a function such that for every z ∈ K and every ξ,

v z - (lambda / 2) * ∑ i, (z i - ξ i)^2 ≤ vhat ξ.

Suppose that equality holds at the pair (η, y), namely

vhat η = v y - (lambda / 2) * ∑ i, (y i - η i)^2.

If (q, Y) belongs to the superjet of vhat at η relative to all of R^n, then (q, Y) belongs to the superjet of v at y relative to K.

theorem ViscositySolns.superjet_gradient_eq_of_supConvolutionMajorant {n : ℕ} {K : Set (Point n)} {v vhat : Point n → ℝ} {lambda : ℝ} {η y q : Point n} {Y : Hessian n} (hmajor : ∀ z ∈ K, ∀ (ξ : Point n), supConvolutionKernel lambda v ξ z ≤ vhat ξ) (hy : y ∈ K) (hvalue : vhat η = supConvolutionKernel lambda v η y) (hJ : { gradient := q, hessian := Y } ∈ Superjet Set.univ vhat η) : q = lambda • (y - η)

The gradient component of a superjet of a function majorizing all sup-convolution kernels is determined by a kernel value where equality holds.

In quantified mathematical form, let vhat : Point n -> Real satisfy

v z - (lambda / 2) * ∑ i, (z i - ξ i)^2 ≤ vhat ξ

for every z ∈ K and every ξ. Suppose that y ∈ K and that equality holds at (η, y), namely

vhat η = v y - (lambda / 2) * ∑ i, (y i - η i)^2.

If (q, Y) ∈ J^{2,+}_{R^n} vhat(η), then

q = lambda • (y - η).

theorem ViscositySolns.superjet_gradient_eq_of_compactSupConvolution_of_isMaxOn {n : ℕ} {K : Set (Point n)} {v : Point n → ℝ} {lambda : ℝ} {η y q : Point n} {Y : Hessian n} (hmax_exists : ∀ (ξ : Point n), ∃ z ∈ K, IsMaxOn (fun (x : Point n) => supConvolutionKernel lambda v ξ x) K z) (hy : y ∈ K) (hmaxη : IsMaxOn (fun (z : Point n) => supConvolutionKernel lambda v η z) K y) (hJ : { gradient := q, hessian := Y } ∈ Superjet Set.univ (fun (ξ : Point n) => compactSupConvolution lambda K v ξ) η) : q = lambda • (y - η)

The gradient component of a superjet of a compact sup-convolution is determined by any point where the defining supremum is attained.

In quantified mathematical form, suppose that for every ξ the function

z ↦ v z - (lambda / 2) * ∑ i, (z i - ξ i)^2

has a maximum point on K. Suppose also that y ∈ K and that y is a maximum point on K for the parameter η. If

(q, Y) ∈ J^{2,+}_{R^n} (ξ ↦ compactSupConvolution lambda K v ξ)(η),

then q = lambda • (y - η).

theorem ViscositySolns.superjet_of_superjet_compactSupConvolution_of_isMaxOn {n : ℕ} {K : Set (Point n)} {v : Point n → ℝ} {lambda : ℝ} {η y q : Point n} {Y : Hessian n} (hmax_exists : ∀ (ξ : Point n), ∃ z ∈ K, IsMaxOn (fun (x : Point n) => supConvolutionKernel lambda v ξ x) K z) (hy : y ∈ K) (hmaxη : IsMaxOn (fun (z : Point n) => supConvolutionKernel lambda v η z) K y) (hJ : { gradient := q, hessian := Y } ∈ Superjet Set.univ (fun (ξ : Point n) => compactSupConvolution lambda K v ξ) η) : { gradient := q, hessian := Y } ∈ Superjet K v y

The compact-set superjet transfer lemma for the compact sup-convolution.

In quantified mathematical form, suppose that for every ξ the function z ↦ v z - (lambda / 2) * ∑ i, (z i - ξ i)^2 has a maximum point on K, and suppose that the maximum at η is attained at y. If (q, Y) belongs to the superjet of ξ ↦ compactSupConvolution lambda K v ξ at η relative to all of R^n, then (q, Y) belongs to the superjet of v at y relative to K.

theorem ViscositySolns.superjet_of_superjet_compactSupConvolution_of_isCompact {n : ℕ} {K : Set (Point n)} {v : Point n → ℝ} {lambda : ℝ} {η y q : Point n} {Y : Hessian n} (hKne : K.Nonempty) (hKcompact : IsCompact K) (hv : UpperSemicontinuousOn v K) (hy : y ∈ K) (hmaxη : IsMaxOn (fun (z : Point n) => supConvolutionKernel lambda v η z) K y) (hJ : { gradient := q, hessian := Y } ∈ Superjet Set.univ (fun (ξ : Point n) => compactSupConvolution lambda K v ξ) η) : { gradient := q, hessian := Y } ∈ Superjet K v y

Compactness and upper semicontinuity supply the maximum points required by the compact-set superjet transfer lemma.

In quantified mathematical form, let K be nonempty and compact, and let v be upper semicontinuous on K. If y ∈ K is a maximum point on K of z ↦ v z - (lambda / 2) * ∑ i, (z i - η i)^2, and if (q, Y) belongs to the superjet of ξ ↦ compactSupConvolution lambda K v ξ at η relative to all of R^n, then (q, Y) belongs to the superjet of v at y relative to K.

noncomputable def ViscositySolns.supConvolutionTransferPoint {n : ℕ} (lambda : ℝ) (ξ : Point n) (J : Jet n) : Point n

The point selected by the formal sup-convolution transfer map.

In the source proof, an ordinary superjet (q, Y) of the sup-convolution at ξ is transferred to the original function at ξ + q / λ. Since Point n is a real vector space, this declaration writes that point as ξ + λ⁻¹ • q.

Equations

• ViscositySolns.supConvolutionTransferPoint lambda ξ J = ξ + lambda⁻¹ • J.gradient

theorem ViscositySolns.supConvolutionTransferPoint_eq_of_compactSupConvolution_of_isMaxOn {n : ℕ} {K : Set (Point n)} {v : Point n → ℝ} {lambda : ℝ} {η y q : Point n} {Y : Hessian n} (hlambda : lambda ≠ 0) (hmax_exists : ∀ (ξ : Point n), ∃ z ∈ K, IsMaxOn (fun (x : Point n) => supConvolutionKernel lambda v ξ x) K z) (hy : y ∈ K) (hmaxη : IsMaxOn (fun (z : Point n) => supConvolutionKernel lambda v η z) K y) (hJ : { gradient := q, hessian := Y } ∈ Superjet Set.univ (fun (ξ : Point n) => compactSupConvolution lambda K v ξ) η) : supConvolutionTransferPoint lambda η { gradient := q, hessian := Y } = y

If lambda ≠ 0, the formal transfer point of a superjet of a compact sup-convolution equals any point where the defining supremum is attained.

In quantified mathematical form, under the hypotheses of superjet_gradient_eq_of_compactSupConvolution_of_isMaxOn, if lambda ≠ 0, then

η + lambda⁻¹ • q = y.