OneStepSchauderWeakId

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

The weak Laplacian identity, the radial Laplacian, and cutoff localization

Three further ingredients of the flux-vanishing crux:

• the weak identity ∫ u · Δψ = ∫ Δu · ψ for globally C² data with one factor compactly supported, obtained from Mathlib's line-derivative integration by parts;
• the radial Laplacian, i.e. the second-derivative calculus of r ↦ f(x+r•ω) used to convert the sphere-average derivative into a flux;
• cutoff localization, which upgrades the globally-C² weak identity to a function harmonic only on a neighbourhood of a closed ball, by multiplying by a smooth bump.

noncomputable def Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.dirDeriv2 {d : ℕ} (v : EuclideanSpace ℝ (Fin d)) (f : EuclideanSpace ℝ (Fin d) → ℝ) (x : EuclideanSpace ℝ (Fin d)) : ℝ

The second directional derivative of f in direction v: ∂ᵥᵥ f (x) = D(y ↦ Df(y)·v)(x)·v. For C² functions this agrees with the iterated Fréchet derivative iterated ℝ 2 f x ![v, v] (see iteratedFDeriv_two_eq_dirDeriv2).

Equations

• Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.dirDeriv2 v f x = (fderiv ℝ (fun (y : EuclideanSpace ℝ (Fin d)) => (fderiv ℝ f y) v) x) v

Smoothness / support bookkeeping for dirDeriv2

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.continuous_dirDeriv2 {d : ℕ} {f : EuclideanSpace ℝ (Fin d) → ℝ} (hf : ContDiff ℝ 2 f) (v : EuclideanSpace ℝ (Fin d)) : Continuous (dirDeriv2 v f)

The second directional derivative of a C² function is continuous.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.hasCompactSupport_dirDeriv2 {d : ℕ} {f : EuclideanSpace ℝ (Fin d) → ℝ} (hf : HasCompactSupport f) (v : EuclideanSpace ℝ (Fin d)) : HasCompactSupport (dirDeriv2 v f)

The second directional derivative of a compactly supported function is compactly supported.

The iterated-derivative ↔ second-directional-derivative bridge

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.iteratedFDeriv_two_eq_dirDeriv2 {d : ℕ} {f : EuclideanSpace ℝ (Fin d) → ℝ} (hf : ContDiff ℝ 2 f) (x v : EuclideanSpace ℝ (Fin d)) : (iteratedFDeriv ℝ 2 f x) ![v, v] = dirDeriv2 v f x

For C² f, the diagonal value of the iterated Fréchet derivative equals the second directional derivative in direction v.

Green's second identity, one direction at a time

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.green_dirDeriv2 {d : ℕ} {u ψ : EuclideanSpace ℝ (Fin d) → ℝ} (hu : ContDiff ℝ 2 u) (hψ : ContDiff ℝ 2 ψ) (hψc : HasCompactSupport ψ) (v : EuclideanSpace ℝ (Fin d)) : ∫ (x : EuclideanSpace ℝ (Fin d)), u x * dirDeriv2 v ψ x = ∫ (x : EuclideanSpace ℝ (Fin d)), dirDeriv2 v u x * ψ x

Green's identity in a single direction. For u ∈ C² and a compactly supported ψ ∈ C², ∫ u · ∂ᵥᵥψ = ∫ ∂ᵥᵥu · ψ. Proved by integrating by parts twice in direction v (integral_mul_fderiv_eq_neg_fderiv_mul_of_integrable); the boundary terms vanish because ψ has compact support.

Green's second identity and the weak harmonic identity

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.integral_mul_laplacian_eq_integral_laplacian_mul {d : ℕ} {u ψ : EuclideanSpace ℝ (Fin d) → ℝ} (hu : ContDiff ℝ 2 u) (hψ : ContDiff ℝ 2 ψ) (hψc : HasCompactSupport ψ) : ∫ (x : EuclideanSpace ℝ (Fin d)), u x * Laplacian.laplacian ψ x = ∫ (x : EuclideanSpace ℝ (Fin d)), Laplacian.laplacian u x * ψ x

Green's second identity. For u ∈ C² and a compactly supported ψ ∈ C², ∫ u · Δψ = ∫ Δu · ψ. Obtained by summing the single-direction Green identity (green_dirDeriv2) over the standard orthonormal coordinate directions and identifying ∑ᵢ ∂ᵢᵢ with the Laplacian.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.dirDeriv2_radial {d : ℕ} {φ : ℝ → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (x₀ y v : EuclideanSpace ℝ (Fin d)) : dirDeriv2 v (fun (z : EuclideanSpace ℝ (Fin d)) => φ (‖z - x₀‖ ^ 2)) y = 4 * inner ℝ (y - x₀) v ^ 2 * deriv (deriv φ) (‖y - x₀‖ ^ 2) + 2 * ‖v‖ ^ 2 * deriv φ (‖y - x₀‖ ^ 2)

Second directional derivative of a radial function. For φ ∈ C^∞ and the radial test ψ(z) = φ(‖z − x₀‖²), the second directional derivative in direction v is dirDeriv2 v ψ y = 4 ⟪y − x₀, v⟫² φ''(‖y−x₀‖²) + 2 ‖v‖² φ'(‖y−x₀‖²).

Computed by restricting to the line t ↦ y + t v, along which ‖(y+t v)−x₀‖² is a quadratic, and applying two 1-D chain rules.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.laplacian_radial {d : ℕ} {φ : ℝ → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (x₀ y : EuclideanSpace ℝ (Fin d)) : Laplacian.laplacian (fun (z : EuclideanSpace ℝ (Fin d)) => φ (‖z - x₀‖ ^ 2)) y = 4 * ‖y - x₀‖ ^ 2 * deriv (deriv φ) (‖y - x₀‖ ^ 2) + 2 * ↑d * deriv φ (‖y - x₀‖ ^ 2)

The radial Laplacian profile. For φ ∈ C^∞ and the radial test ψ(y) = φ(‖y − x₀‖²), Δψ(y) = 4 ‖y − x₀‖² · φ''(‖y−x₀‖²) + 2 d · φ'(‖y−x₀‖²).

Obtained by summing dirDeriv2_radial over the standard orthonormal basis and using Parseval ∑ᵢ ⟪y−x₀, eᵢ⟫² = ‖y−x₀‖² together with ∑ᵢ ‖eᵢ‖² = d.

The one-dimensional radial profiles

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.deriv_radialProfile {φ : ℝ → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (r : ℝ) : deriv (fun (s : ℝ) => φ (s ^ 2)) r = 2 * r * deriv φ (r ^ 2)

The radial profile p(r) = φ(r²) of ψ(y) = φ(‖y − x₀‖²) has derivative p'(r) = 2 r · φ'(r²).

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.hasDerivAt_weighted_radialProfile {d : ℕ} {φ : ℝ → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hd : 1 ≤ d) (r : ℝ) : HasDerivAt (fun (s : ℝ) => s ^ (d - 1) * (2 * s * deriv φ (s ^ 2))) (r ^ (d - 1) * (4 * r ^ 2 * deriv (deriv φ) (r ^ 2) + 2 * ↑d * deriv φ (r ^ 2))) r

The load-bearing 1-D radial identity (r^{d−1} p'(r))' = r^{d−1} m(r), in IBP-ready HasDerivAt form. Here p(r) = φ(r²) is the radial profile of ψ(y) = φ(‖y − x₀‖²) (so p'(r) = 2 r φ'(r²), cf. deriv_radialProfile) and m(r) = 4 r² φ''(r²) + 2 d φ'(r²)

is the radial profile of Δψ (cf. laplacian_radial, evaluated at ‖y − x₀‖ = r). This is the total-derivative structure the flux-vanishing assembly integrates by parts against in the radial variable. Pure one-dimensional calculus (no inner-product geometry).

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.integral_mul_laplacian_eq_zero_of_harmonicOn {d : ℕ} {u ψ : EuclideanSpace ℝ (Fin d) → ℝ} {x : EuclideanSpace ℝ (Fin d)} {r R : ℝ} (hr : 0 < r) (hrR : r < R) (hu : InnerProductSpace.HarmonicOnNhd u (Metric.ball x R)) (hψ : ContDiff ℝ 2 ψ) (hψc : HasCompactSupport ψ) (hsupp : tsupport ψ ⊆ Metric.ball x r) : ∫ (y : EuclideanSpace ℝ (Fin d)), u y * Laplacian.laplacian ψ y = 0

Cutoff localization of the weak harmonic identity. If u is harmonic on the open ball Metric.ball x R and ψ ∈ C² has compact support inside a strictly smaller ball tsupport ψ ⊆ Metric.ball x r (0 < r < R), then ∫ u · Δψ = 0.

This is the local version of integral_mul_laplacian_eq_zero_of_harmonic: u need only be harmonic near the closed ball, not on all of space.