HarmonicGreen

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

Green's second identity for the coordinate Laplacian on Vec d

Mathlib's harmonic-function layer (Analysis/InnerProductSpace/Harmonic/*) is stated for InnerProductSpace, which the sup-normed carrier Vec ddoes **not** satisfy; and Mathlib's only divergence theorem is the box form onFin (n+1) -> R. CoarseGraining, however, already carries a *coordinate* Laplacian on Vec d--euclideanCoordLaplacian u x = sum_i d_i d_i u x, built from euclideanCoordDeriv i u x = fderiv R u x (basisVec i)in `Sobolev/Foundations/EuclideanL2 -- and Mathlib carries a global integration-by-parts identity valid on any finite-dimensional real normed space with an additive Haar measure, in particular on Vec d with Lebesgue measure.

Iterating that identity twice in each coordinate direction and summing gives Green's second identity for the coordinate Laplacian, with no EuclideanSpace transfer and no boundary term. This is the pairing that defines the weak (distributional) formulation of Delta u = 0.

Contents

• contDiff_euclideanCoordDeriv_of_contDiff_succ and continuous_euclideanCoordLaplacian_of_contDiff_two -- the finite-regularity companions of CoarseGraining's C^infty-only smoothness lemmas.
• integral_mul_euclideanCoordDeriv_eq_neg_of_contDiff_one -- one integration by parts, int u d_i psi = - int (d_i u) psi.
• integral_mul_euclideanCoordSecondDeriv_eq -- two integrations by parts, int u d_i d_i psi = int (d_i d_i u) psi.
• integral_mul_euclideanCoordLaplacian_eq_integral_euclideanCoordLaplacian_mul -- Green's second identity int u (Delta psi) = int (Delta u) psi for a C^2 function u and a compactly supported C^2 test function psi.
• integral_mul_euclideanCoordLaplacian_eq_zero_of_forall_mem -- the consequence used to feed the weak formulation: if the coordinate Laplacian of u vanishes on an set containing tsupport psi, then the pairing int u (Delta psi) vanishes.

Every hypothesis is a genuine regularity or support hypothesis on the two functions; there is no boundary term because the test function has compact support and the identity is taken over the whole space.

References

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

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.contDiff_euclideanCoordDeriv_of_contDiff_succ {d : ℕ} {ψ : HCPolySupport.Vec d → ℝ} {n : ℕ} (hψ : ContDiff ℝ (↑(n + 1)) ψ) (i : Fin d) : ContDiff ℝ (↑n) (HCPolySupport.euclideanCoordDeriv i ψ)

Coordinate differentiation at finite regularity.

CoarseGraining proves contDiff_euclideanCoordDeriv only at C^infty; the two-fold integration by parts below needs the finite-level statement that a coordinate derivative of a C^{n+1} function is C^n.

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.integral_mul_euclideanCoordDeriv_eq_neg_of_contDiff_one {d : ℕ} {u ψ : HCPolySupport.Vec d → ℝ} (hu : ContDiff ℝ (↑1) u) (hψ : ContDiff ℝ (↑1) ψ) (hψc : HasCompactSupport ψ) (i : Fin d) : ∫ (x : HCPolySupport.Vec d), u x * HCPolySupport.euclideanCoordDeriv i ψ x = -∫ (x : HCPolySupport.Vec d), HCPolySupport.euclideanCoordDeriv i u x * ψ x

One integration by parts in a coordinate direction.

int u * (d_i psi) = - int (d_i u) * psi, with no boundary term because psi has compact support. This is Mathlib's global Haar-measure integration by parts specialized to the direction basisVec i on Vec d.

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.integral_mul_euclideanCoordSecondDeriv_eq {d : ℕ} {u ψ : HCPolySupport.Vec d → ℝ} (hu : ContDiff ℝ (↑2) u) (hψ : ContDiff ℝ (↑2) ψ) (hψc : HasCompactSupport ψ) (i : Fin d) : ∫ (x : HCPolySupport.Vec d), u x * HCPolySupport.euclideanCoordSecondDeriv i i ψ x = ∫ (x : HCPolySupport.Vec d), HCPolySupport.euclideanCoordSecondDeriv i i u x * ψ x

Two integrations by parts in the same coordinate direction.

int u * (d_i d_i psi) = int (d_i d_i u) * psi. The two sign changes cancel.

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.continuous_euclideanCoordLaplacian_of_contDiff_two {d : ℕ} {u : HCPolySupport.Vec d → ℝ} (hu : ContDiff ℝ (↑2) u) : Continuous (HCPolySupport.euclideanCoordLaplacian u)

The coordinate Laplacian of a C^2 function is continuous. CoarseGraining proves contDiff_euclideanCoordLaplacian only at C^infty.

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.integral_mul_euclideanCoordLaplacian_eq_integral_euclideanCoordLaplacian_mul {d : ℕ} {u ψ : HCPolySupport.Vec d → ℝ} (hu : ContDiff ℝ (↑2) u) (hψ : ContDiff ℝ (↑2) ψ) (hψc : HasCompactSupport ψ) : ∫ (x : HCPolySupport.Vec d), u x * HCPolySupport.euclideanCoordLaplacian ψ x = ∫ (x : HCPolySupport.Vec d), HCPolySupport.euclideanCoordLaplacian u x * ψ x

Green's second identity for the coordinate Laplacian.

int u * (Delta psi) = int (Delta u) * psi for u of class C^2 and a compactly supported C^2 test function psi. Summing the two-fold coordinate integration by parts over the d directions.

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.integral_mul_euclideanCoordLaplacian_eq_zero_of_forall_mem {d : ℕ} {U : Set (HCPolySupport.Vec d)} {u ψ : HCPolySupport.Vec d → ℝ} (hu : ContDiff ℝ (↑2) u) (hψ : ContDiff ℝ (↑2) ψ) (hψc : HasCompactSupport ψ) (hsupp : tsupport ψ ⊆ U) (hzero : ∀ x ∈ U, HCPolySupport.euclideanCoordLaplacian u x = 0) : ∫ (x : HCPolySupport.Vec d), u x * HCPolySupport.euclideanCoordLaplacian ψ x = 0

The vanishing pairing.

If the coordinate Laplacian of a C^2 function u vanishes at every point of a set containing the support of the test function, then the Green pairing int u (Delta psi) vanishes. This is the statement that a classically harmonic function is harmonic in the distributional sense.