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

Euclidean geometry on Point n

Point n = Fin n → ℝ carries the sup norm, but the Laplace barriers are radial for the Euclidean distance. This file records the squared Euclidean distance eucSq x y = (x - y) ⬝ᵥ (x - y) and the uniform exterior sphere condition phrased with it.

def ViscositySolns.eucSq {n : ℕ} (x y : Point n) : ℝ

Squared Euclidean distance on Point n.

Equations

• ViscositySolns.eucSq x y = (x - y) ⬝ᵥ (x - y)

theorem ViscositySolns.eucSq_nonneg {n : ℕ} (x y : Point n) : 0 ≤ eucSq x y

theorem ViscositySolns.eucSq_comm {n : ℕ} (x y : Point n) : eucSq x y = eucSq y x

theorem ViscositySolns.eucSq_self {n : ℕ} (x : Point n) : eucSq x x = 0

theorem ViscositySolns.continuous_eucSq {n : ℕ} : Continuous fun (q : Point n × Point n) => eucSq q.1 q.2

def ViscositySolns.UniformExteriorSphereSq {n : ℕ} (C : Set (Point n)) (R : ℝ) : Prop

Uniform exterior sphere condition with radius R, in squared Euclidean distance: every frontier point x₀ of C lies on a sphere of radius R centred at some y, and closure C lies outside the open ball.

Equations

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