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

Sup-convolution declarations (ClosedJetTransfer)

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.supConvolutionTransferValue {n : ℕ} (lambda : ℝ) (ξ : Point n) (r : ℝ) (J : Jet n) : ℝ

The value component of the graph map used in the closed-superjet transfer.

If r is the sup-convolution value at ξ and y = supConvolutionTransferPoint lambda ξ J, then the corresponding value of the original function is expected to be

r + (lambda / 2) * ∑ i, (y i - ξ i)^2.

Equations

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

noncomputable def ViscositySolns.supConvolutionTransferGraphPoint {n : ℕ} (lambda : ℝ) (z : (Point n × ℝ) × Jet n) : (Point n × ℝ) × Jet n

The graph map used to pass from closed superjets of a compact sup-convolution to closed superjets of the original function.

Equations

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

theorem ViscositySolns.continuous_supConvolutionTransferGraphPoint {n : ℕ} (lambda : ℝ) : Continuous fun (z : (Point n × ℝ) × Jet n) => supConvolutionTransferGraphPoint lambda z

The sup-convolution graph-transfer map is continuous.

theorem ViscositySolns.mem_closure_superjetGraph_value_le_of_upperSemicontinuousOn {n : ℕ} {K : Set (Point n)} {v : Point n → ℝ} {z : (Point n × ℝ) × Jet n} (hKclosed : IsClosed K) (hv : UpperSemicontinuousOn v K) (hz : z ∈ closure (SuperjetGraph K v)) : z.1.1 ∈ K ∧ z.1.2 ≤ v z.1.1

At a closure point of the superjet graph of an upper semicontinuous function, the limiting value is bounded above by the function value at the limiting base point.

In quantified mathematical form, if K is closed, v is upper semicontinuous on K, and ((x, r), J) belongs to the closure of SuperjetGraph K v, then x ∈ K and r ≤ v x.

theorem ViscositySolns.supConvolutionTransferValue_eq_of_mem_closure_superjetGraph_of_isCompact {n : ℕ} {K : Set (Point n)} {v : Point n → ℝ} {lambda : ℝ} {η : Point n} {J : Jet n} (hKne : K.Nonempty) (hKcompact : IsCompact K) (hv : UpperSemicontinuousOn v K) (hclosure : supConvolutionTransferGraphPoint lambda ((η, compactSupConvolution lambda K v η), J) ∈ closure (SuperjetGraph K v)) : v (supConvolutionTransferPoint lambda η J) = compactSupConvolution lambda K v η + lambda / 2 * (supConvolutionTransferPoint lambda η J - η) ⬝ᵥ (supConvolutionTransferPoint lambda η J - η)

The value identity for a transfer graph point lying in the closure of the superjet graph of the original function.

In quantified mathematical form, suppose K is nonempty and compact, v is upper semicontinuous on K, and

supConvolutionTransferGraphPoint lambda ((η, compactSupConvolution lambda K v η), J)

belongs to the closure of SuperjetGraph K v. Then

`v (η + lambda⁻¹ • J.gradient) = compactSupConvolution lambda K v η

• (lambda / 2) * ∑ i, ((η + lambda⁻¹ • J.gradient) i - η i)^2`.

theorem ViscositySolns.closedSuperjet_of_closedSuperjet_compactSupConvolution_transfer {n : ℕ} {K : Set (Point n)} {v : Point n → ℝ} {lambda : ℝ} {η : Point n} {J : Jet n} (hmax_exists : ∀ (ξ : Point n), ∃ z ∈ K, IsMaxOn (fun (x : Point n) => supConvolutionKernel lambda v ξ x) K z) (hselected : ∀ (ξ : Point n), ∀ J' ∈ Superjet Set.univ (fun (ζ : Point n) => compactSupConvolution lambda K v ζ) ξ, supConvolutionTransferPoint lambda ξ J' ∈ K ∧ IsMaxOn (fun (z : Point n) => supConvolutionKernel lambda v ξ z) K (supConvolutionTransferPoint lambda ξ J')) (hvalue : v (supConvolutionTransferPoint lambda η J) = compactSupConvolution lambda K v η + lambda / 2 * (supConvolutionTransferPoint lambda η J - η) ⬝ᵥ (supConvolutionTransferPoint lambda η J - η)) (hJ : J ∈ ClosedSuperjet Set.univ (fun (ξ : Point n) => compactSupConvolution lambda K v ξ) η) : J ∈ ClosedSuperjet K v (supConvolutionTransferPoint lambda η J)

Closed-superjet transfer for the compact sup-convolution, stated with explicit ordinary-graph selection hypotheses.

In quantified mathematical form, suppose that every compact sup-convolution kernel has a maximum point on K. Suppose also that for every ordinary superjet (q, Y) of the compact sup-convolution at ξ, the point ξ + lambda⁻¹ • q belongs to K and is a maximum point of z ↦ v z - (lambda / 2) * ∑ i, (z i - ξ i)^2 on K. If (p, X) belongs to the closed superjet of the compact sup-convolution at η, and if the value identity

`v (η + lambda⁻¹ • p) = compactSupConvolution lambda K v η

• (lambda / 2) * ∑ i, ((η + lambda⁻¹ • p) i - η i)^2`

holds, then (p, X) belongs to the closed superjet of v at η + lambda⁻¹ • p relative to K.

theorem ViscositySolns.closedSuperjet_of_closedSuperjet_compactSupConvolution_transfer_of_isCompact {n : ℕ} {K : Set (Point n)} {v : Point n → ℝ} {lambda : ℝ} {η : Point n} {J : Jet n} (hKne : K.Nonempty) (hKcompact : IsCompact K) (hv : UpperSemicontinuousOn v K) (hselected : ∀ (ξ : Point n), ∀ J' ∈ Superjet Set.univ (fun (ζ : Point n) => compactSupConvolution lambda K v ζ) ξ, supConvolutionTransferPoint lambda ξ J' ∈ K ∧ IsMaxOn (fun (z : Point n) => supConvolutionKernel lambda v ξ z) K (supConvolutionTransferPoint lambda ξ J')) (hvalue : v (supConvolutionTransferPoint lambda η J) = compactSupConvolution lambda K v η + lambda / 2 * (supConvolutionTransferPoint lambda η J - η) ⬝ᵥ (supConvolutionTransferPoint lambda η J - η)) (hJ : J ∈ ClosedSuperjet Set.univ (fun (ξ : Point n) => compactSupConvolution lambda K v ξ) η) : J ∈ ClosedSuperjet K v (supConvolutionTransferPoint lambda η J)

Compactness and upper semicontinuity supply the kernel maximum points required by the closed-superjet transfer theorem.

In quantified mathematical form, let K be nonempty and compact, and let v be upper semicontinuous on K. Suppose that for every ordinary superjet (q, Y) of the compact sup-convolution at ξ, the point ξ + lambda⁻¹ • q belongs to K and is a maximum point on K of z ↦ v z - (lambda / 2) * ∑ i, (z i - ξ i)^2. If (p, X) belongs to the closed superjet of the compact sup-convolution at η, and if the corresponding value identity holds at η + lambda⁻¹ • p, then (p, X) belongs to the closed superjet of v at that point relative to K.

theorem ViscositySolns.closedSuperjet_of_closedSuperjet_compactSupConvolution_transfer_of_isCompact_of_value {n : ℕ} {K : Set (Point n)} {v : Point n → ℝ} {lambda : ℝ} {η : Point n} {J : Jet n} (hlambda : lambda ≠ 0) (hKne : K.Nonempty) (hKcompact : IsCompact K) (hv : UpperSemicontinuousOn v K) (hvalue : v (supConvolutionTransferPoint lambda η J) = compactSupConvolution lambda K v η + lambda / 2 * (supConvolutionTransferPoint lambda η J - η) ⬝ᵥ (supConvolutionTransferPoint lambda η J - η)) (hJ : J ∈ ClosedSuperjet Set.univ (fun (ξ : Point n) => compactSupConvolution lambda K v ξ) η) : J ∈ ClosedSuperjet K v (supConvolutionTransferPoint lambda η J)

Closed-superjet transfer for compact sup-convolutions, with the ordinary superjet maximum-point hypothesis discharged by the gradient identity.

In quantified mathematical form, let K be nonempty and compact, let v be upper semicontinuous on K, and let lambda ≠ 0. If (p, X) belongs to the closed superjet of ξ ↦ compactSupConvolution lambda K v ξ at η, and if

`v (η + lambda⁻¹ • p) = compactSupConvolution lambda K v η

• (lambda / 2) * ∑ i, ((η + lambda⁻¹ • p) i - η i)^2`,

then (p, X) belongs to the closed superjet of v at η + lambda⁻¹ • p relative to K.

theorem ViscositySolns.closedSuperjet_of_closedSuperjet_compactSupConvolution_transfer_of_isCompact_of_ne_zero {n : ℕ} {K : Set (Point n)} {v : Point n → ℝ} {lambda : ℝ} {η : Point n} {J : Jet n} (hlambda : lambda ≠ 0) (hKne : K.Nonempty) (hKcompact : IsCompact K) (hv : UpperSemicontinuousOn v K) (hJ : J ∈ ClosedSuperjet Set.univ (fun (ξ : Point n) => compactSupConvolution lambda K v ξ) η) : J ∈ ClosedSuperjet K v (supConvolutionTransferPoint lambda η J)

Closed-superjet transfer for compact sup-convolutions.

In quantified mathematical form, let K be nonempty and compact, let v be upper semicontinuous on K, and let lambda ≠ 0. If (p, X) belongs to the closed superjet of ξ ↦ compactSupConvolution lambda K v ξ at η, then (p, X) belongs to the closed superjet of v at η + lambda⁻¹ • p relative to K.

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

The compact-set inf-convolution value.

In standard mathematical notation this is

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

It is defined by negating the compact sup-convolution of -v, so that the closed-subjet transfer theorem below is the exact dual of the closed-superjet transfer theorem for compact sup-convolutions.

Equations

• ViscositySolns.compactInfConvolution lambda K v ξ = -ViscositySolns.compactSupConvolution lambda K (fun (x : ViscositySolns.Point n) => -v x) ξ

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

The function whose infimum defines the inf-convolution at ξ.

In standard mathematical notation this is

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

Equations

• ViscositySolns.infConvolutionKernel lambda v ξ x = v x + lambda / 2 * (x - ξ) ⬝ᵥ (x - ξ)

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

The point selected by the compact inf-convolution transfer map.

In standard mathematical notation, a subjet with first-order part p at η transfers to the point η - λ⁻¹ p.

Equations

• ViscositySolns.infConvolutionTransferPoint lambda η J = η - lambda⁻¹ • J.gradient

theorem ViscositySolns.compactInfConvolution_eq_neg_compactSupConvolution_neg {n : ℕ} {K : Set (Point n)} {v : Point n → ℝ} {lambda : ℝ} {η : Point n} : compactInfConvolution lambda K v η = -compactSupConvolution lambda K (fun (x : Point n) => -v x) η

The compact inf-convolution is the negative of the compact sup-convolution of the negated function.

theorem ViscositySolns.infConvolutionKernel_eq_neg_supConvolutionKernel_neg {n : ℕ} (lambda : ℝ) (v : Point n → ℝ) (ξ x : Point n) : infConvolutionKernel lambda v ξ x = -supConvolutionKernel lambda (fun (z : Point n) => -v z) ξ x

The inf-convolution kernel is the negative of the sup-convolution kernel for the negated function.

theorem ViscositySolns.lowerSemicontinuousOn_infConvolutionKernel {n : ℕ} {K : Set (Point n)} {v : Point n → ℝ} {lambda : ℝ} {ξ : Point n} (hv : LowerSemicontinuousOn v K) : LowerSemicontinuousOn (fun (x : Point n) => infConvolutionKernel lambda v ξ x) K

If v is lower semicontinuous on K, then the inf-convolution kernel is lower semicontinuous on K.

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

theorem ViscositySolns.exists_isMinOn_infConvolutionKernel_of_isCompact {n : ℕ} {K : Set (Point n)} {v : Point n → ℝ} {lambda : ℝ} {ξ : Point n} (hKne : K.Nonempty) (hKcompact : IsCompact K) (hv : LowerSemicontinuousOn v K) : ∃ x ∈ K, IsMinOn (fun (y : Point n) => infConvolutionKernel lambda v ξ y) K x

On a nonempty compact set, the inf-convolution kernel attains a minimum.

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

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

theorem ViscositySolns.compactInfConvolution_eq_of_isMinOn {n : ℕ} {K : Set (Point n)} {v : Point n → ℝ} {lambda : ℝ} {ξ y : Point n} (hy : y ∈ K) (hmin : IsMinOn (fun (z : Point n) => infConvolutionKernel lambda v ξ z) K y) : compactInfConvolution lambda K v ξ = infConvolutionKernel lambda v ξ y

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

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

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

then

compactInfConvolution lambda K v ξ = v y + (lambda / 2) * ∑ i, (y i - ξ i)^2.

theorem ViscositySolns.infConvolutionTransferPoint_eq_supConvolutionTransferPoint_neg {n : ℕ} {lambda : ℝ} {η : Point n} {J : Jet n} : infConvolutionTransferPoint lambda η J = supConvolutionTransferPoint lambda η J.neg

The compact inf-convolution transfer point is the compact sup-convolution transfer point for the negated jet and negated function.

theorem ViscositySolns.lowerSemicontinuousOn_neg_to_upperSemicontinuousOn {n : ℕ} {K : Set (Point n)} {v : Point n → ℝ} (hv : LowerSemicontinuousOn v K) : UpperSemicontinuousOn (fun (x : Point n) => -v x) K

Lower semicontinuity of v gives upper semicontinuity of -v.

This local theorem keeps the compact inf-convolution transfer independent of the viscosity-solution declarations.

theorem ViscositySolns.closedSubjet_of_closedSubjet_compactInfConvolution_transfer_of_isCompact_of_ne_zero {n : ℕ} {K : Set (Point n)} {v : Point n → ℝ} {lambda : ℝ} {η : Point n} {J : Jet n} (hlambda : lambda ≠ 0) (hKne : K.Nonempty) (hKcompact : IsCompact K) (hv : LowerSemicontinuousOn v K) (hJ : J ∈ ClosedSubjet Set.univ (fun (ξ : Point n) => compactInfConvolution lambda K v ξ) η) : J ∈ ClosedSubjet K v (infConvolutionTransferPoint lambda η J)

Closed-subjet transfer for compact inf-convolutions.

In quantified mathematical form, let K be nonempty and compact, let v be lower semicontinuous on K, and let lambda ≠ 0. If (p, X) belongs to the closed subjet of

η ↦ inf { v(x) + (lambda / 2) * ∑ i, (x i - η i)^2 | x ∈ K }

at η relative to all of R^n, then (p, X) belongs to the closed subjet of v at η - lambda⁻¹ • p relative to K.