HarmonicInteriorGradient

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

The interior gradient estimate for the coordinate Laplacian on Vec d

Mathlib has no interior gradient estimate for harmonic functions outside the complex plane, and its harmonic layer is stated for InnerProductSpace R E, which the sup-normed carrier Vec d does not satisfy. This module proves the estimate natively for CoarseGraining's euclideanCoordLaplacian, in the dimensional form

  |d_i u (z)| <= C (d) / r * avg_{B (z, r)} |u| .

The proof needs neither the divergence theorem nor a surface measure. It runs the kernel mean value property of HarmonicMeanValue on the harmonic function d_i u and then moves the derivative onto the kernel with the single integration by parts of HarmonicGreen:

1. d_i u is harmonic. For a C^infty function, CoarseGraining's euclideanCoordThirdDeriv_diag_right_comm gives d_j d_j d_i u = d_i d_j d_j u pointwise, so the coordinate Laplacian of d_i u is the i-th coordinate derivative of the coordinate Laplacian of u, which vanishes identically on the open set where u is harmonic.
2. A C^1 annulus kernel. posPartSq s = (max 0 s)^2 is C^1 with derivative 2 max 0 s -- the only delicate point being the corner at the origin, where the slope is computed directly -- so gradKernel a b t = posPartSq (t - a) * posPartSq (b - t) is a C^1 nonnegative kernel supported in [a, b], positive on (a, b), with the explicit derivative bound |gradKernel' | <= 4 (b - a)^3.
3. The pairing. With a = r/4 and b = r/2, the mean value property gives d_i u (z) * int K = int (d_i u) K, integration by parts turns the right side into - int u (d_i K), and |d_i K| <= 4 (b - a)^3 on the ball of radius b < r yields |d_i u (z)| * int K <= 4 (b - a)^3 * int_{B (z, r)} |u|.
4. The scaling. The kernel mass is bounded below on the explicit annulus 5 r / 16 < |x - z| < 7 r / 16, where gradKernel >= (r/16)^4, by the ball volumes of HarmonicGauge; the resulting lower bound is proportional to r^(d + 4), which is exactly what turns the estimate into the stated C (d) / r form. The unit ball volume cancels, leaving the explicit admissible constant 4096 / ((7/16)^d - (6/16)^d).

Contents

• posPartSq, hasDerivAt_posPartSq, contDiff_posPartSq -- the C^1 one-sided square.
• gradKernel, gradKernelDeriv, hasDerivAt_gradKernel, pow_four_le_gradKernel, abs_gradKernelDeriv_le -- the C^1 annulus kernel with its lower bound and its derivative bound.
• euclideanCoordLaplacian_euclideanCoordDeriv_eq_zero -- a coordinate derivative of a harmonic function is harmonic.
• exists_interior_gradient_bound -- the interior gradient estimate.

Regularity

exists_interior_gradient_bound assumes ContDiff R (top : Nat-infinity) u. The third-derivative symmetry it needs is available in CoarseGraining only at C^infty (euclideanCoordSecondDeriv_comm, euclideanCoordThirdDeriv_diag_right_comm), so the hypothesis is stated at that level; harmonic functions are smooth, but this module proves no regularity theorem and therefore cannot weaken the hypothesis on its own.

References

• ABK26, e.nablaw.oscillations (the eventual consumer).

The C^1 one-sided square

noncomputable def Algsuperdiff.Section3.Provider.Diffusivity.Corrector.posPartSq (s : ℝ) : ℝ

The square of the positive part: s ↦ (max 0 s)^2.

Equations

• Algsuperdiff.Section3.Provider.Diffusivity.Corrector.posPartSq s = max 0 s * max 0 s

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.posPartSq_nonneg (s : ℝ) : 0 ≤ posPartSq s

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.posPartSq_eq_zero_of_nonpos {s : ℝ} (hs : s ≤ 0) : posPartSq s = 0

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.posPartSq_eq_of_nonneg {s : ℝ} (hs : 0 ≤ s) : posPartSq s = s * s

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.hasDerivAt_posPartSq (s : ℝ) : HasDerivAt posPartSq (2 * max 0 s) s

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.contDiff_posPartSq : ContDiff ℝ 1 posPartSq

The C^1 annulus kernel

noncomputable def Algsuperdiff.Section3.Provider.Diffusivity.Corrector.gradKernel (a b t : ℝ) : ℝ

The C^1 radial kernel (max 0 (t - a))^2 (max 0 (b - t))^2 supported in [a, b].

Equations

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

noncomputable def Algsuperdiff.Section3.Provider.Diffusivity.Corrector.gradKernelDeriv (a b t : ℝ) : ℝ

The derivative of gradKernel.

Equations

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

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.hasDerivAt_gradKernel (a b t : ℝ) : HasDerivAt (gradKernel a b) (gradKernelDeriv a b t) t

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.contDiff_gradKernel (a b : ℝ) : ContDiff ℝ 1 (gradKernel a b)

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.continuous_gradKernel (a b : ℝ) : Continuous (gradKernel a b)

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.gradKernel_nonneg (a b t : ℝ) : 0 ≤ gradKernel a b t

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.gradKernel_eq_zero_of_le {a b t : ℝ} (ht : t ≤ a) : gradKernel a b t = 0

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.gradKernel_eq_zero_of_ge {a b t : ℝ} (ht : b ≤ t) : gradKernel a b t = 0

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.gradKernel_pos {a b t : ℝ} (h1 : a < t) (h2 : t < b) : 0 < gradKernel a b t

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.pow_four_le_gradKernel {a b t c : ℝ} (hc : 0 ≤ c) (h1 : a + c ≤ t) (h2 : t + c ≤ b) : c ^ 4 ≤ gradKernel a b t

A quantitative lower bound on gradKernel well inside its annulus.

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.abs_gradKernelDeriv_le {a b : ℝ} (hab : a ≤ b) (t : ℝ) : |gradKernelDeriv a b t| ≤ 4 * (b - a) ^ 3

The uniform bound on the derivative of gradKernel.

Harmonicity of a coordinate derivative

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.euclideanCoordLaplacian_euclideanCoordDeriv_eq_zero {d : ℕ} {u : HCPolySupport.Vec d → ℝ} (hu : ContDiff ℝ (↑⊤) u) {U : Set (HCPolySupport.Vec d)} (hU : IsOpen U) (hharm : ∀ y ∈ U, HCPolySupport.euclideanCoordLaplacian u y = 0) {x : HCPolySupport.Vec d} (hx : x ∈ U) (i : Fin d) : HCPolySupport.euclideanCoordLaplacian (HCPolySupport.euclideanCoordDeriv i u) x = 0

A coordinate derivative of a harmonic function is harmonic.

The interior gradient estimate

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.exists_interior_gradient_bound {d : ℕ} (hd : 0 < d) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (u : HCPolySupport.Vec d → ℝ), ContDiff ℝ (↑⊤) u → ∀ (r : ℝ), 0 < r → ∀ (z : HCPolySupport.Vec d), (∀ x ∈ HCPolySupport.euclideanBall z r, HCPolySupport.euclideanCoordLaplacian u x = 0) → ∀ (i : Fin d), |HCPolySupport.euclideanCoordDeriv i u z| ≤ C / r * ((∫ (x : HCPolySupport.Vec d) in HCPolySupport.euclideanBall z r, |u x|) / (MeasureTheory.volume (HCPolySupport.euclideanBall z r)).toReal)

The interior gradient estimate for the coordinate Laplacian on Vec d.