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

Transport between EuclideanSpace ℝ (Fin d) and Point d

The viscosity theory in this repository lives on Point d = Fin d → ℝ with the sup norm, while the harmonic-function statements are phrased on EuclideanSpace ℝ (Fin d) with Mathlib's Laplacian. The coordinate map toPoint is a continuous linear equivalence (so it preserves topology, boundedness, and Lebesgue measure), and it converts Euclidean distances into eucSq.

• eucSq_toPoint: eucSq (toPoint x) (toPoint y) = dist x y ^ 2.
• UniformExteriorSphere.image_toPoint: the exterior sphere condition transfers to UniformExteriorSphereSq.
• laplacian_eq_lapTrace: Mathlib's Laplacian is the coordinate trace of the second derivative in Point d.
• weaklyHarmonicOn_of_forall_integral_lapTrace: the weak harmonicity statement in Point d coordinates gives WeaklyHarmonicOn on the Euclidean side.

@[reducible, inline]

abbrev ViscositySolns.toPoint {d : ℕ} : EuclideanSpace ℝ (Fin d) ≃L[ℝ] Point d

The coordinate map EuclideanSpace ℝ (Fin d) ≃L[ℝ] Point d.

Equations

• ViscositySolns.toPoint = PiLp.continuousLinearEquiv 2 ℝ fun (x : Fin d) => ℝ

@[simp]

theorem ViscositySolns.toPoint_apply {d : ℕ} (x : EuclideanSpace ℝ (Fin d)) (i : Fin d) : toPoint x i = x.ofLp i

theorem ViscositySolns.eucSq_toPoint {d : ℕ} (x y : EuclideanSpace ℝ (Fin d)) : eucSq (toPoint x) (toPoint y) = dist x y ^ 2

theorem ViscositySolns.eucSq_eq_dist_symm {d : ℕ} (x y : Point d) : eucSq x y = dist (toPoint.symm x) (toPoint.symm y) ^ 2

theorem ViscositySolns.image_toPoint_frontier {d : ℕ} (U : Set (EuclideanSpace ℝ (Fin d))) : ⇑toPoint '' frontier U = frontier (⇑toPoint '' U)

theorem ViscositySolns.image_toPoint_closure {d : ℕ} (U : Set (EuclideanSpace ℝ (Fin d))) : ⇑toPoint '' closure U = closure (⇑toPoint '' U)

theorem ViscositySolns.isOpen_image_toPoint {d : ℕ} {U : Set (EuclideanSpace ℝ (Fin d))} (hU : IsOpen U) : IsOpen (⇑toPoint '' U)

theorem ViscositySolns.isBounded_image_toPoint {d : ℕ} {U : Set (EuclideanSpace ℝ (Fin d))} (hU : Bornology.IsBounded U) : Bornology.IsBounded (⇑toPoint '' U)

theorem ViscositySolns.UniformExteriorSphere.image_toPoint {d : ℕ} {U : Set (EuclideanSpace ℝ (Fin d))} (hU : UniformExteriorSphere U) : ∃ (R : ℝ), UniformExteriorSphereSq (⇑toPoint '' U) R

The Euclidean exterior sphere condition in Point d coordinates.

theorem ViscositySolns.LipschitzOnWith.abs_sub_le_eucSq {d : ℕ} {U : Set (EuclideanSpace ℝ (Fin d))} {g : EuclideanSpace ℝ (Fin d) → ℝ} {L : NNReal} (hg : LipschitzOnWith L g (closure U)) (x : Point d) : x ∈ closure (⇑toPoint '' U) → ∀ y ∈ closure (⇑toPoint '' U), |g (toPoint.symm x) - g (toPoint.symm y)| ≤ ↑L * √(eucSq x y)

A Euclidean-Lipschitz function gives the eucSq Lipschitz bound in Point d.

theorem ViscositySolns.toPoint_single {d : ℕ} (i : Fin d) : toPoint (EuclideanSpace.single i 1) = Pi.single i 1

theorem ViscositySolns.laplacian_eq_lapTrace {d : ℕ} {χ : EuclideanSpace ℝ (Fin d) → ℝ} (hχ : ContDiff ℝ 2 χ) (x : EuclideanSpace ℝ (Fin d)) : Laplacian.laplacian χ x = lapTrace (χ ∘ ⇑toPoint.symm) (toPoint x)

Mathlib's Laplacian is the coordinate trace of the second derivative after passing to Point d coordinates.

theorem ViscositySolns.weaklyHarmonicOn_of_forall_integral_lapTrace {d : ℕ} {U : Set (EuclideanSpace ℝ (Fin d))} {w : Point d → ℝ} (hw : ∀ (χ : Point d → ℝ), ContDiff ℝ (↑⊤) χ → HasCompactSupport χ → tsupport χ ⊆ ⇑toPoint '' U → ∫ (x : Point d), lapTrace χ x * w x = 0) : Analysis.WeaklyHarmonicOn MeasureTheory.volume (w ∘ ⇑toPoint) U

Weak harmonicity in Point d coordinates, tested against the coordinate trace lapTrace, gives Mathlib's WeaklyHarmonicOn for the transported function on EuclideanSpace ℝ (Fin d).