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

Radial test functions for Laplace barriers

This file collects the analytic ingredients of the exterior-sphere barriers for the Laplace operator.

• Euclidean geometry on Point n (which carries the sup norm): the square root of eucSq is the EuclideanSpace distance, so it satisfies the triangle inequality, and eucSq is comparable to the sup norm.
• A scalar Peano form of Taylor's theorem of order two.
• The second-order expansion of a radial function x ↦ G (eucSq x c): if G has the expansion G s₀ + G₁ (s - s₀) + G₂ (s - s₀)² / 2 + o((s - s₀)²) at s₀ = |x̂ - c|², then x ↦ G (eucSq x c) has the jet (2 G₁ z, 2 G₁ I + 4 G₂ z zᵀ) at x̂, where z = x̂ - c.
• The exponential profile s ↦ a - k exp (-α (s - ρ)), whose radial Hessian has trace 2 k α e (n - 2 α s₀).
• Trace comparison: a subjet and a superjet of the same function at an interior point have ordered traces.

Euclidean geometry on Point n

theorem ViscositySolns.sqrt_eucSq_eq_dist {n : ℕ} (x y : Point n) : √(eucSq x y) = dist (WithLp.toLp 2 x) (WithLp.toLp 2 y)

The square root of eucSq is the distance in EuclideanSpace.

theorem ViscositySolns.sqrt_eucSq_triangle {n : ℕ} (x y z : Point n) : √(eucSq x z) ≤ √(eucSq x y) + √(eucSq y z)

Triangle inequality for the Euclidean distance √(eucSq x y).

theorem ViscositySolns.eucSq_eq_sqrt_sq {n : ℕ} (x y : Point n) : eucSq x y = √(eucSq x y) ^ 2

theorem ViscositySolns.eucSq_pos_of_ne {n : ℕ} {x y : Point n} (h : x ≠ y) : 0 < eucSq x y

theorem ViscositySolns.norm_sub_le_sqrt_eucSq {n : ℕ} (x y : Point n) : ‖x - y‖ ≤ √(eucSq x y)

The sup norm is dominated by the Euclidean distance.

theorem ViscositySolns.eucSq_le_card_mul_norm_sq {n : ℕ} (x y : Point n) : eucSq x y ≤ ↑n * ‖x - y‖ ^ 2

The Euclidean distance is dominated by n times the sup norm (squared).

theorem ViscositySolns.abs_dotProduct_le {n : ℕ} (a b : Point n) : |a ⬝ᵥ b| ≤ ↑n * (‖a‖ * ‖b‖)

theorem ViscositySolns.eucSq_midpoint {n : ℕ} (x x₀ y : Point n) : eucSq x ((1 / 2) • (x₀ + y)) = eucSq x₀ y / 4 + eucSq x x₀ / 2 + (eucSq x y - eucSq x₀ y) / 2

Squared distance to the midpoint (x₀ + y) / 2: |x - (x₀ + y)/2|² = |x₀ - y|²/4 + |x - x₀|²/2 + (|x - y|² - |x₀ - y|²)/2.

theorem ViscositySolns.eucSq_sub_eucSq_base {n : ℕ} (x x₀ c : Point n) : eucSq x c - eucSq x₀ c = 2 * (x₀ - c) ⬝ᵥ (x - x₀) + (x - x₀) ⬝ᵥ (x - x₀)

Expansion of eucSq around a base point.

Trace comparison of semijets

theorem ViscositySolns.trace_eq_sum_quadraticForm {n : ℕ} (M : Hessian n) : Matrix.trace M = ∑ i : Fin n, Matrix.mulVec M (Pi.single i 1) ⬝ᵥ Pi.single i 1

theorem ViscositySolns.trace_nonneg_of_mem_superjet_zero_univ {n : ℕ} {x : Point n} {K : Jet n} (hK : K ∈ Superjet Set.univ (fun (x : Point n) => 0) x) : 0 ≤ Matrix.trace K.hessian

A full-neighbourhood superjet of the zero function has nonnegative trace.

theorem ViscositySolns.trace_hessian_le_of_mem_subjet_of_mem_superjet {n : ℕ} {C : Set (Point n)} {u : Point n → ℝ} {x : Point n} {J K : Jet n} (hx : x ∈ interior C) (hJ : J ∈ Subjet C u x) (hK : K ∈ Superjet C u x) : Matrix.trace J.hessian ≤ Matrix.trace K.hessian

At an interior point, the trace of any subjet is at most the trace of any superjet of the same function.

Scalar Taylor expansion

theorem ViscositySolns.isLittleO_taylor_two_of_hasDerivAt {G G' : ℝ → ℝ} {s₀ G₂ : ℝ} (hG : ∀ (s : ℝ), HasDerivAt G (G' s) s) (hG' : HasDerivAt G' G₂ s₀) : (fun (s : ℝ) => G s - (G s₀ + G' s₀ * (s - s₀) + G₂ / 2 * (s - s₀) ^ 2)) =o[nhds s₀] fun (s : ℝ) => (s - s₀) ^ 2

Peano form of the second-order Taylor expansion of a scalar function whose derivative is differentiable at the base point.

Radial functions

def ViscositySolns.radialJet {n : ℕ} (G₁ G₂ : ℝ) (z : Point n) : Jet n

The second-order jet of x ↦ G (eucSq x c) at a point with z = x̂ - c.

Equations

• ViscositySolns.radialJet G₁ G₂ z = { gradient := (2 * G₁) • z, hessian := (2 * G₁) • 1 + (4 * G₂) • Matrix.vecMulVec z z }

theorem ViscositySolns.trace_radialJet_hessian {n : ℕ} (G₁ G₂ : ℝ) (z : Point n) : Matrix.trace (radialJet G₁ G₂ z).hessian = 2 * G₁ * ↑n + 4 * G₂ * z ⬝ᵥ z

theorem ViscositySolns.quadraticModel_radialJet {n : ℕ} (x₀ : Point n) (r G₁ G₂ : ℝ) (z x : Point n) : quadraticModel x₀ r (radialJet G₁ G₂ z).gradient (radialJet G₁ G₂ z).hessian x = r + G₁ * (2 * z ⬝ᵥ (x - x₀) + (x - x₀) ⬝ᵥ (x - x₀)) + 2 * G₂ * (z ⬝ᵥ (x - x₀)) ^ 2

theorem ViscositySolns.hasSecondOrderExpansionWithin_comp_eucSq {n : ℕ} {C : Set (Point n)} {G : ℝ → ℝ} {G₁ G₂ : ℝ} {c x₀ : Point n} (hG : (fun (s : ℝ) => G s - (G (eucSq x₀ c) + G₁ * (s - eucSq x₀ c) + G₂ / 2 * (s - eucSq x₀ c) ^ 2)) =o[nhds (eucSq x₀ c)] fun (s : ℝ) => (s - eucSq x₀ c) ^ 2) : HasSecondOrderExpansionWithin C (fun (x : Point n) => G (eucSq x c)) x₀ (radialJet G₁ G₂ (x₀ - c))

Second-order expansion of a radial function x ↦ G (eucSq x c) from a scalar second-order Peano expansion of G at s₀ = eucSq x̂ c.

The exponential profile

noncomputable def ViscositySolns.expProfile (a k α ρ s : ℝ) : ℝ

The exponential radial profile s ↦ a - k exp (-α (s - ρ)).

Equations

• ViscositySolns.expProfile a k α ρ s = a - k * Real.exp (-(α * (s - ρ)))

theorem ViscositySolns.hasDerivAt_expProfile (a k α ρ s : ℝ) : HasDerivAt (expProfile a k α ρ) (k * α * Real.exp (-(α * (s - ρ)))) s

theorem ViscositySolns.hasDerivAt_expProfile_deriv (k α ρ s : ℝ) : HasDerivAt (fun (s : ℝ) => k * α * Real.exp (-(α * (s - ρ)))) (-(k * α ^ 2 * Real.exp (-(α * (s - ρ))))) s

noncomputable def ViscositySolns.expProfileJet {n : ℕ} (k α ρ : ℝ) (c x₀ : Point n) : Jet n

The radial jet of the exponential profile at x₀.

Equations

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

theorem ViscositySolns.hasSecondOrderExpansionWithin_expProfile {n : ℕ} (C : Set (Point n)) (a k α ρ : ℝ) (c x₀ : Point n) : HasSecondOrderExpansionWithin C (fun (x : Point n) => expProfile a k α ρ (eucSq x c)) x₀ (expProfileJet k α ρ c x₀)

theorem ViscositySolns.trace_expProfileJet_hessian {n : ℕ} (k α ρ : ℝ) (c x₀ : Point n) : Matrix.trace (expProfileJet k α ρ c x₀).hessian = 2 * k * α * Real.exp (-(α * (eucSq x₀ c - ρ))) * (↑n - 2 * α * eucSq x₀ c)

theorem ViscositySolns.trace_expProfileJet_hessian_nonpos {n : ℕ} {k α ρ : ℝ} (hk : 0 ≤ k) (hα : 0 ≤ α) {c x₀ : Point n} (hs : ↑n ≤ 2 * α * eucSq x₀ c) : Matrix.trace (expProfileJet k α ρ c x₀).hessian ≤ 0

Radial superharmonicity of the exponential profile when k ≥ 0.

Scalar inequalities for the barrier profile

theorem ViscositySolns.sqrt_le_sqrt_add_div {a b : ℝ} (ha : 0 ≤ a) (hb : 0 < b) : √a ≤ √b + (a - b) / (2 * √b)

Concavity of the square root: √a ≤ √b + (a - b) / (2 √b).

theorem ViscositySolns.one_sub_exp_neg_le (u : ℝ) : 1 - Real.exp (-u) ≤ u

theorem ViscositySolns.mul_exp_neg_le_one_sub_exp_neg (u : ℝ) : u * Real.exp (-u) ≤ 1 - Real.exp (-u)