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

Foundational definitions for viscosity solutions

This file contains the ambient coordinate model, jets, quadratic models, and abstract second-order expansion predicates used throughout the formalization.

@[reducible, inline]

abbrev ViscositySolns.Point (n : ℕ) : Type

The ambient Euclidean coordinate space R^n, represented as functions on Fin n.

Equations

• ViscositySolns.Point n = (Fin n → ℝ)

theorem ViscositySolns.nhdsWithin_eq_of_subset_of_mem_nhdsWithin {α : Type u_1} [TopologicalSpace α] {K C : Set α} {x : α} (hKC : K ⊆ C) (hK : K ∈ nhdsWithin x C) : nhdsWithin x K = nhdsWithin x C

theorem ViscositySolns.eventually_mem_nhdsWithin_of_mem_nhdsWithin_of_tendsto {α : Type u_1} {ι : Type u_2} [TopologicalSpace α] {K C : Set α} {x : α} {xᵢ : ι → α} {l : Filter ι} (hK : K ∈ nhdsWithin x C) (hx : Filter.Tendsto xᵢ l (nhds x)) (hmem : ∀ᶠ (i : ι) in l, xᵢ i ∈ C) : ∀ᶠ (i : ι) in l, K ∈ nhdsWithin (xᵢ i) C

@[reducible, inline]

abbrev ViscositySolns.Hessian (n : ℕ) : Type

Hessian matrices for scalar equations on R^n.

Equations

• ViscositySolns.Hessian n = Matrix (Fin n) (Fin n) ℝ

structure ViscositySolns.Jet (n : ℕ) : Type

First and second derivative data used in the second-order semijets.

• gradient : Point n

  First derivative in coordinate form.

• hessian : Hessian n

  Second derivative in coordinate matrix form.

@[reducible, inline]

abbrev ViscositySolns.Operator (n : ℕ) : Type

A scalar fully nonlinear second-order operator F(x, r, p, X).

Equations

• ViscositySolns.Operator n = (ViscositySolns.Point n → ℝ → ViscositySolns.Point n → ViscositySolns.Hessian n → ℝ)

def ViscositySolns.Jet.equivProd (n : ℕ) : Jet n ≃ Point n × Hessian n

Jets are equivalent to their gradient/Hessian product data.

Equations

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

@[instance_reducible]

instance ViscositySolns.Jet.instTopologicalSpace {n : ℕ} : TopologicalSpace (Jet n)

The product topology on jets, induced by their gradient and Hessian components.

Equations

• ViscositySolns.Jet.instTopologicalSpace = TopologicalSpace.induced (fun (J : ViscositySolns.Jet n) => (J.gradient, J.hessian)) inferInstance

theorem ViscositySolns.Jet.continuous_gradient {n : ℕ} : Continuous fun (J : Jet n) => J.gradient

The gradient projection from jets is continuous.

theorem ViscositySolns.Jet.continuous_hessian {n : ℕ} : Continuous fun (J : Jet n) => J.hessian

The Hessian projection from jets is continuous.

@[instance_reducible]

instance ViscositySolns.Jet.instZero {n : ℕ} : Zero (Jet n)

The zero jet has zero first- and second-order parts.

Equations

• ViscositySolns.Jet.instZero = (ViscositySolns.Jet.equivProd n).zero

@[simp]

theorem ViscositySolns.Jet.zero_gradient {n : ℕ} : gradient 0 = 0

@[simp]

theorem ViscositySolns.Jet.zero_hessian {n : ℕ} : hessian 0 = 0

@[instance_reducible]

instance ViscositySolns.Jet.instAdd {n : ℕ} : Add (Jet n)

Jets add componentwise.

Equations

• ViscositySolns.Jet.instAdd = { add := fun (J K : ViscositySolns.Jet n) => { gradient := J.gradient + K.gradient, hessian := J.hessian + K.hessian } }

@[instance_reducible]

instance ViscositySolns.Jet.instAddCommGroup {n : ℕ} : AddCommGroup (Jet n)

Jets form an additive commutative group under componentwise addition.

Equations

• ViscositySolns.Jet.instAddCommGroup = (ViscositySolns.Jet.equivProd n).addCommGroup

@[simp]

theorem ViscositySolns.Jet.add_gradient {n : ℕ} (J K : Jet n) : (J + K).gradient = J.gradient + K.gradient

@[simp]

theorem ViscositySolns.Jet.add_hessian {n : ℕ} (J K : Jet n) : (J + K).hessian = J.hessian + K.hessian

@[simp]

theorem ViscositySolns.Jet.neg_gradient' {n : ℕ} (J : Jet n) : (-J).gradient = -J.gradient

@[simp]

theorem ViscositySolns.Jet.neg_hessian' {n : ℕ} (J : Jet n) : (-J).hessian = -J.hessian

@[simp]

theorem ViscositySolns.Jet.sub_gradient {n : ℕ} (J K : Jet n) : (J - K).gradient = J.gradient - K.gradient

@[simp]

theorem ViscositySolns.Jet.sub_hessian {n : ℕ} (J K : Jet n) : (J - K).hessian = J.hessian - K.hessian

@[instance_reducible]

instance ViscositySolns.Jet.instSMul {n : ℕ} : SMul ℝ (Jet n)

Scalar multiplication of jets is componentwise.

Equations

• ViscositySolns.Jet.instSMul = { smul := fun (a : ℝ) (J : ViscositySolns.Jet n) => { gradient := a • J.gradient, hessian := a • J.hessian } }

@[simp]

theorem ViscositySolns.Jet.smul_gradient {n : ℕ} (a : ℝ) (J : Jet n) : (a • J).gradient = a • J.gradient

@[simp]

theorem ViscositySolns.Jet.smul_hessian {n : ℕ} (a : ℝ) (J : Jet n) : (a • J).hessian = a • J.hessian

def ViscositySolns.Jet.neg {n : ℕ} (J : Jet n) : Jet n

Negating a jet negates both first- and second-order parts.

Equations

• J.neg = { gradient := -J.gradient, hessian := -J.hessian }

@[simp]

theorem ViscositySolns.Jet.neg_gradient {n : ℕ} (J : Jet n) : J.neg.gradient = -J.gradient

@[simp]

theorem ViscositySolns.Jet.neg_hessian {n : ℕ} (J : Jet n) : J.neg.hessian = -J.hessian

@[simp]

theorem ViscositySolns.Jet.neg_eq_neg {n : ℕ} (J : Jet n) : -J = J.neg

noncomputable def ViscositySolns.quadraticModel {n : ℕ} (x0 : Point n) (r : ℝ) (p : Point n) (X : Hessian n) (x : Point n) : ℝ

The quadratic polynomial determined by a value, gradient, and Hessian at x0, evaluated at x.

Equations

• ViscositySolns.quadraticModel x0 r p X x = r + p ⬝ᵥ (x - x0) + 1 / 2 * Matrix.mulVec X (x - x0) ⬝ᵥ (x - x0)

noncomputable def ViscositySolns.quadraticModelJetAt {n : ℕ} (x0 p : Point n) (X : Hessian n) (x : Point n) : Jet n

The jet obtained by re-expanding a fixed quadratic polynomial at a new base point.

In standard coordinates, if q(z) = r + p · (z - x0) + 1 / 2 (X (z - x0)) · (z - x0), then at x its second-order part is still X, and its first-order part is p + 1 / 2 (X + Xᵀ) (x - x0).

Equations

• ViscositySolns.quadraticModelJetAt x0 p X x = { gradient := p + (1 / 2) • (Matrix.mulVec X (x - x0) + (Matrix.transpose X).mulVec (x - x0)), hessian := X }

@[simp]

theorem ViscositySolns.quadraticModelJetAt_base {n : ℕ} (x0 p : Point n) (X : Hessian n) : quadraticModelJetAt x0 p X x0 = { gradient := p, hessian := X }

theorem ViscositySolns.quadraticModel_recenter {n : ℕ} (x0 : Point n) (r : ℝ) (p : Point n) (X : Hessian n) (x y : Point n) : quadraticModel x0 r p X y = quadraticModel x (quadraticModel x0 r p X x) (quadraticModelJetAt x0 p X x).gradient (quadraticModelJetAt x0 p X x).hessian y

Re-expanding a quadratic model at any point gives the same polynomial.

noncomputable def ViscositySolns.symHessian {n : ℕ} (X : Hessian n) : Hessian n

The symmetric part of a Hessian matrix.

Equations

• ViscositySolns.symHessian X = (1 / 2) • (X + Matrix.transpose X)

@[simp]

theorem ViscositySolns.symHessian_apply {n : ℕ} (X : Hessian n) (i j : Fin n) : symHessian X i j = 1 / 2 * (X i j + X j i)

theorem ViscositySolns.symHessian_isHermitian {n : ℕ} (X : Hessian n) : Matrix.IsHermitian (symHessian X)

The symmetric part of a real Hessian is Hermitian.

theorem ViscositySolns.symHessian_eq_self_of_isHermitian {n : ℕ} {X : Hessian n} (hX : Matrix.IsHermitian X) : symHessian X = X

Symmetrizing a Hermitian real Hessian leaves it unchanged.

theorem ViscositySolns.quadraticModel_symHessian {n : ℕ} (x0 : Point n) (r : ℝ) (p : Point n) (X : Hessian n) (x : Point n) : quadraticModel x0 r p (symHessian X) x = quadraticModel x0 r p X x

The quadratic model depends only on the symmetric part of its Hessian.

This records the classical fact that vᵀ X v = vᵀ ((X + Xᵀ) / 2) v.

theorem ViscositySolns.quadraticModelJetAt_gradient_symHessian {n : ℕ} (x0 p : Point n) (X : Hessian n) (x : Point n) : (quadraticModelJetAt x0 p (symHessian X) x).gradient = (quadraticModelJetAt x0 p X x).gradient

Recentered quadratic-model gradients are unchanged by Hessian symmetrization.

theorem ViscositySolns.point_abs_apply_le_norm {n : ℕ} (v : Point n) (i : Fin n) : |v i| ≤ ‖v‖

Every coordinate of a point is bounded by the finite Pi sup norm.

theorem ViscositySolns.dotProduct_self_le_card_mul_norm_sq {n : ℕ} (v : Point n) : v ⬝ᵥ v ≤ ↑n * ‖v‖ ^ 2

The Euclidean coordinate quadratic form is controlled by the finite Pi sup norm, with the dimension as the comparison constant.

theorem ViscositySolns.abs_dotProduct_le_card_mul_norm_mul_norm {n : ℕ} (u v : Point n) : |u ⬝ᵥ v| ≤ ↑n * ‖u‖ * ‖v‖

The coordinate dot product is bounded by the product of the finite Pi norms, up to the dimension factor.

theorem ViscositySolns.norm_sq_le_dotProduct_self {n : ℕ} (v : Point n) : ‖v‖ ^ 2 ≤ v ⬝ᵥ v

The finite Pi sup norm is controlled by the Euclidean coordinate quadratic form. This includes the case n = 0, where both sides are zero.

theorem ViscositySolns.quadraticModel_scalar_identity_bound {n : ℕ} (x0 x : Point n) {a : ℝ} (ha : 0 ≤ a) : quadraticModel x0 0 0 (a • 1) x ≤ 1 / 2 * a * ↑n * ‖x - x0‖ ^ 2

A positive scalar multiple of the identity Hessian contributes only a controlled second-order term. The constant reflects that Point n uses the Pi sup norm.

theorem ViscositySolns.quadraticModel_scalar_identity_lower_bound {n : ℕ} (x0 x : Point n) {a : ℝ} (ha : 0 ≤ a) : 1 / 2 * a * ‖x - x0‖ ^ 2 ≤ quadraticModel x0 0 0 (a • 1) x

A positive scalar multiple of the identity Hessian dominates the square of the finite Pi sup norm, with coefficient a / 2.

theorem ViscositySolns.continuous_hessian_apply_apply {n : ℕ} (i j : Fin n) : Continuous fun (X : Hessian n) => X i j

Evaluation at a Hessian entry is continuous.

theorem ViscositySolns.hessian_eventually_entrywise_abs_sub_lt {n : ℕ} (X : Hessian n) {η : ℝ} (hη : 0 < η) : ∀ᶠ (Y : Hessian n) in nhds X, ∀ (i j : Fin n), |(Y - X) i j| < η

For every η > 0, the set of matrices Y such that |(Y - X) i j| < η for all entries i j is a neighborhood of X. This packages the product topology on Hessian n into the finite entrywise form used by semijet closure arguments.

theorem ViscositySolns.abs_quadraticModel_zero_zero_le_of_entrywise_abs_le {n : ℕ} (x0 x : Point n) {A : Hessian n} {η : ℝ} (_hη : 0 ≤ η) (hA : ∀ (i j : Fin n), |A i j| ≤ η) : |quadraticModel x0 0 0 A x| ≤ 1 / 2 * η * ↑n * ↑n * ‖x - x0‖ ^ 2

If a Hessian has all entries bounded by η, then its quadratic model is bounded by a dimension-dependent multiple of η ‖x - x0‖².

theorem ViscositySolns.continuous_quadraticModel_jet {n : ℕ} (x0 : Point n) (r : ℝ) (x : Point n) : Continuous fun (J : Jet n) => quadraticModel x0 r J.gradient J.hessian x

For fixed base point, value, and evaluation point, the quadratic model varies continuously with the jet data.

theorem ViscositySolns.continuous_quadraticModel {n : ℕ} (x0 : Point n) (r : ℝ) (p : Point n) (X : Hessian n) : Continuous fun (x : Point n) => quadraticModel x0 r p X x

For fixed jet data, the quadratic model is a continuous function of the evaluation point.

@[simp]

theorem ViscositySolns.quadraticModel_neg {n : ℕ} (x0 : Point n) (r : ℝ) (p : Point n) (X : Hessian n) (x : Point n) : quadraticModel x0 (-r) (-p) (-X) x = -quadraticModel x0 r p X x

Negating the value, gradient, and Hessian data negates the quadratic model.

theorem ViscositySolns.quadraticModel_add {n : ℕ} (x0 : Point n) (r s : ℝ) (p q : Point n) (X Y : Hessian n) (x : Point n) : quadraticModel x0 (r + s) (p + q) (X + Y) x = quadraticModel x0 r p X x + quadraticModel x0 s q Y x

The quadratic model is additive in its value, gradient, and Hessian data.

theorem ViscositySolns.quadraticModel_sub {n : ℕ} (x0 : Point n) (r s : ℝ) (p q : Point n) (X Y : Hessian n) (x : Point n) : quadraticModel x0 (r - s) (p - q) (X - Y) x = quadraticModel x0 r p X x - quadraticModel x0 s q Y x

The quadratic model is subtractive in its value, gradient, and Hessian data.

theorem ViscositySolns.quadraticModel_mixed_second_difference {n : ℕ} (x0 : Point n) (r : ℝ) (p : Point n) (X : Hessian n) (u v : Point n) : quadraticModel x0 r p X (x0 + u + v) - quadraticModel x0 r p X (x0 + u) - quadraticModel x0 r p X (x0 + v) + quadraticModel x0 r p X x0 = 1 / 2 * (Matrix.mulVec X u ⬝ᵥ v + Matrix.mulVec X v ⬝ᵥ u)

The mixed second difference of a quadratic model depends only on the Hessian.

In standard mathematical terms, for a quadratic polynomial q(x) = r + p · (x - x0) + (1 / 2)⟪X(x - x0), x - x0⟫, the expression

q(x0 + u + v) - q(x0 + u) - q(x0 + v) + q(x0)

is

(1 / 2) * (⟪Xu, v⟫ + ⟪Xv, u⟫).

theorem ViscositySolns.quadraticModel_convexCombination {n : ℕ} (x0 : Point n) (r a b : ℝ) (p q : Point n) (X Y : Hessian n) (x : Point n) (hab : a + b = 1) : quadraticModel x0 r (a • p + b • q) (a • X + b • Y) x = a * quadraticModel x0 r p X x + b * quadraticModel x0 r q Y x

The quadratic model is affine in its jet data when the base value is fixed.

theorem ViscositySolns.quadraticModel_le_of_hessian_le {n : ℕ} {x0 : Point n} {r : ℝ} {p : Point n} {X Y : Hessian n} (hXY : X ≤ Y) (x : Point n) : quadraticModel x0 r p X x ≤ quadraticModel x0 r p Y x

The quadratic model is monotone in the Hessian for the Loewner order.

def ViscositySolns.SemijetRemainder {n : ℕ} (C : Set (Point n)) (x0 : Point n) (rho : Point n → ℝ) : Prop

The little-oh remainder used in the definition of second-order semijets, relative to a domain C.

Equations

• ViscositySolns.SemijetRemainder C x0 rho = rho =o[nhdsWithin x0 C] fun (x : ViscositySolns.Point n) => ‖x - x0‖ ^ 2

theorem ViscositySolns.semijetRemainder_congr_nhdsWithin {n : ℕ} {C D : Set (Point n)} {x0 : Point n} {rho : Point n → ℝ} (h : nhdsWithin x0 C = nhdsWithin x0 D) : SemijetRemainder C x0 rho ↔ SemijetRemainder D x0 rho

theorem ViscositySolns.semijetRemainder_add {n : ℕ} {C : Set (Point n)} {x0 : Point n} {rho sigma : Point n → ℝ} (hrho : SemijetRemainder C x0 rho) (hsigma : SemijetRemainder C x0 sigma) : SemijetRemainder C x0 fun (x : Point n) => rho x + sigma x

theorem ViscositySolns.semijetRemainder_neg {n : ℕ} {C : Set (Point n)} {x0 : Point n} {rho : Point n → ℝ} (hrho : SemijetRemainder C x0 rho) : SemijetRemainder C x0 fun (x : Point n) => -rho x

theorem ViscositySolns.semijetRemainder_sub {n : ℕ} {C : Set (Point n)} {x0 : Point n} {rho sigma : Point n → ℝ} (hrho : SemijetRemainder C x0 rho) (hsigma : SemijetRemainder C x0 sigma) : SemijetRemainder C x0 fun (x : Point n) => rho x - sigma x

theorem ViscositySolns.semijetRemainder_const_mul {n : ℕ} {C : Set (Point n)} {x0 : Point n} {rho : Point n → ℝ} (a : ℝ) (hrho : SemijetRemainder C x0 rho) : SemijetRemainder C x0 fun (x : Point n) => a * rho x

theorem ViscositySolns.semijetRemainder_along_affine_isLittleO_sq {n : ℕ} {rho : Point n → ℝ} {z a : Point n} (hrho : SemijetRemainder Set.univ z rho) : (fun (t : ℝ) => rho (z + t • a)) =o[nhds 0] fun (t : ℝ) => t ^ 2

A second-order remainder remains o(t^2) along every affine line through its base point.

In standard mathematical terms, if ρ(w) = o(|w - z|^2) as w -> z, then for every vector a,

ρ(z + t a) = o(t^2) as t -> 0.

theorem ViscositySolns.semijetRemainder_mixed_along_affine_isLittleO_sq {n : ℕ} {rho : Point n → ℝ} {z u v : Point n} (hrho : SemijetRemainder Set.univ z rho) (hrho_z : rho z = 0) : (fun (t : ℝ) => rho (z + t • u + t • v) - rho (z + t • u) - rho (z + t • v) + rho z) =o[nhds 0] fun (t : ℝ) => t ^ 2

The mixed second difference of a second-order remainder is o(t^2) along two fixed directions.

In standard mathematical terms, if ρ(w) = o(|w - z|^2) as w -> z and ρ(z) = 0, then for all vectors u and v,

ρ(z + t u + t v) - ρ(z + t u) - ρ(z + t v) + ρ(z) = o(t^2).

def ViscositySolns.HasSecondOrderExpansionWithinAtValue {n : ℕ} (C : Set (Point n)) (φ : Point n → ℝ) (x0 : Point n) (r : ℝ) (J : Jet n) : Prop

φ has second-order expansion with prescribed value r and jet J, relative to the domain C.

Equations

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

theorem ViscositySolns.secondOrderExpansion_remainder_at_base {n : ℕ} {C : Set (Point n)} {φ rho : Point n → ℝ} {x0 : Point n} {r : ℝ} {J : Jet n} (hx0 : x0 ∈ C) (hφ : ∀ᶠ (x : Point n) in nhdsWithin x0 C, φ x = quadraticModel x0 r J.gradient J.hessian x + rho x) : rho x0 = φ x0 - r

The remainder in a second-order expansion has the forced value at the base point.

In standard mathematical terms, if

φ(x) = r + p · (x - x₀) + (1 / 2)⟪X(x - x₀), x - x₀⟫ + ρ(x)

for all x sufficiently close to x₀ inside C, and if x₀ ∈ C, then ρ(x₀) = φ(x₀) - r.

theorem ViscositySolns.secondOrderExpansion_remainder_eq_zero_at_base {n : ℕ} {C : Set (Point n)} {φ rho : Point n → ℝ} {x0 : Point n} {J : Jet n} (hx0 : x0 ∈ C) (hφ : ∀ᶠ (x : Point n) in nhdsWithin x0 C, φ x = quadraticModel x0 (φ x0) J.gradient J.hessian x + rho x) : rho x0 = 0

For an expansion whose prescribed value is the value of the function at the base point, the remainder vanishes at the base point.

theorem ViscositySolns.hasSecondOrderExpansionWithinAtValue_congr_nhdsWithin {n : ℕ} {C D : Set (Point n)} {φ : Point n → ℝ} {x0 : Point n} {r : ℝ} {J : Jet n} (h : nhdsWithin x0 C = nhdsWithin x0 D) : HasSecondOrderExpansionWithinAtValue C φ x0 r J ↔ HasSecondOrderExpansionWithinAtValue D φ x0 r J

def ViscositySolns.HasSecondOrderExpansionWithin {n : ℕ} (C : Set (Point n)) (φ : Point n → ℝ) (x0 : Point n) (J : Jet n) : Prop

φ has second-order expansion at x0 with jet J, relative to the domain C.

This is the abstraction used for smooth test functions: later, a Taylor theorem for C^2 functions can be used to build this predicate from differentiability data.

Equations

• ViscositySolns.HasSecondOrderExpansionWithin C φ x0 J = ViscositySolns.HasSecondOrderExpansionWithinAtValue C φ x0 (φ x0) J

theorem ViscositySolns.hasSecondOrderExpansionWithin_congr_nhdsWithin {n : ℕ} {C D : Set (Point n)} {φ : Point n → ℝ} {x0 : Point n} {J : Jet n} (h : nhdsWithin x0 C = nhdsWithin x0 D) : HasSecondOrderExpansionWithin C φ x0 J ↔ HasSecondOrderExpansionWithin D φ x0 J

theorem ViscositySolns.hasSecondOrderExpansionWithin_quadraticModel_recenter {n : ℕ} {C : Set (Point n)} (x0 : Point n) (r : ℝ) (p : Point n) (X : Hessian n) (x : Point n) : HasSecondOrderExpansionWithin C (fun (y : Point n) => quadraticModel x0 r p X y) x (quadraticModelJetAt x0 p X x)

The recentered jet of a quadratic model gives an exact second-order expansion.

A quadratic polynomial has zero Taylor remainder when it is expanded at any point, with the recentered jet quadraticModelJetAt.

theorem ViscositySolns.continuous_quadraticModelJetAt {n : ℕ} (x0 p : Point n) (X : Hessian n) : Continuous fun (x : Point n) => quadraticModelJetAt x0 p X x

theorem ViscositySolns.tendsto_quadraticModelJetAt_zero_zero_gradient_zero {n : ℕ} (X : Hessian n) : Filter.Tendsto (fun (x : Point n) => (quadraticModelJetAt 0 0 X x).gradient) (nhds 0) (nhds 0)

As x -> 0, the gradient component of the recentered quadratic model with base point 0 and first-order component 0 tends to 0.

def ViscositySolns.TouchesAboveOn {n : ℕ} (C : Set (Point n)) (u φ : Point n → ℝ) (x0 : Point n) : Prop

φ touches u from above at x0, relative to C.

Equations

• ViscositySolns.TouchesAboveOn C u φ x0 = ∀ᶠ (x : ViscositySolns.Point n) in nhdsWithin x0 C, u x - φ x ≤ u x0 - φ x0

theorem ViscositySolns.touchesAboveOn_congr_nhdsWithin {n : ℕ} {C D : Set (Point n)} {u φ : Point n → ℝ} {x0 : Point n} (h : nhdsWithin x0 C = nhdsWithin x0 D) : TouchesAboveOn C u φ x0 ↔ TouchesAboveOn D u φ x0

def ViscositySolns.TouchesBelowOn {n : ℕ} (C : Set (Point n)) (u φ : Point n → ℝ) (x0 : Point n) : Prop

φ touches u from below at x0, relative to C.

Equations

• ViscositySolns.TouchesBelowOn C u φ x0 = ∀ᶠ (x : ViscositySolns.Point n) in nhdsWithin x0 C, u x0 - φ x0 ≤ u x - φ x

theorem ViscositySolns.touchesBelowOn_congr_nhdsWithin {n : ℕ} {C D : Set (Point n)} {u φ : Point n → ℝ} {x0 : Point n} (h : nhdsWithin x0 C = nhdsWithin x0 D) : TouchesBelowOn C u φ x0 ↔ TouchesBelowOn D u φ x0