HarmonicWeak

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

Weak (distributional) harmonicity on Vec d

Mathlib's InnerProductSpace.HarmonicAt is a C^2-strong notion on an inner product space, so it is unavailable on the sup-normed carrier Vec d and it cannot express harmonicity of a merely locally integrable function. CoarseGraining carries the variational notion (IsAHarmonicGradient, phrased through H1Function and IsSolenoidalOn) but no distributional one.

This module fixes the distributional predicate directly on Vec d, using CoarseGraining's coordinate Laplacian and the Green pairing of HarmonicGreen:

  IsWeaklyHarmonicOn U u  <->  int_U u * (Delta psi) = 0
      for every  psi in C_c^infty  with  tsupport psi subset U .

and proves one half of its consistency with the classical notion: a C^2 function that is weakly harmonic on an open set has vanishing coordinate Laplacian there. Green's identity turns the defining pairing into int (Delta u) psi = 0 for every test function supported in U; the fundamental lemma of the calculus of variations (IsOpen.ae_eq_zero_of_integral_contDiff_smul_eq_zero) then gives Delta u = 0 almost everywhere on U, and continuity upgrades that from "almost everywhere on U" to "everywhere on U".

Only that half and the elementary stability properties are proved here. The two substantial theorems about the predicate -- the mean value property and Weyl's lemma (a weakly harmonic function agrees a.e. with a smooth one) -- are not proved here and are not assumed anywhere below.

Contents

• IsWeaklyHarmonicOn -- the predicate.
• setIntegral_mul_euclideanCoordLaplacian_eq_integral -- the Green pairing over U agrees with the pairing over the whole space, because the test function is supported in U.
• IsWeaklyHarmonicOn.euclideanCoordLaplacian_eq_zero -- weak plus C^2 implies classical, on an open set.
• IsWeaklyHarmonicOn.mono, IsWeaklyHarmonicOn.const_mul -- stability under shrinking the set and under scalar multiples.

References

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

def Algsuperdiff.Section3.Provider.Diffusivity.Corrector.IsWeaklyHarmonicOn {d : ℕ} (U : Set (HCPolySupport.Vec d)) (u : HCPolySupport.Vec d → ℝ) : Prop

Weak (distributional) harmonicity on an open set.

u is weakly harmonic on U when its Green pairing against the coordinate Laplacian of every compactly supported smooth test function supported in U vanishes. The test-function class and the int_U convention are those of CoarseGraining's HasWeakPartialDerivOn, so the predicate composes with CoarseGraining's weak-derivative layer without translation.

Equations

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

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.setIntegral_mul_euclideanCoordLaplacian_eq_integral {d : ℕ} {U : Set (HCPolySupport.Vec d)} (u : HCPolySupport.Vec d → ℝ) {ψ : HCPolySupport.Vec d → ℝ} (hsupp : tsupport ψ ⊆ U) : ∫ (x : HCPolySupport.Vec d) in U, u x * HCPolySupport.euclideanCoordLaplacian ψ x = ∫ (x : HCPolySupport.Vec d), u x * HCPolySupport.euclideanCoordLaplacian ψ x

The Green pairing over U is the Green pairing over the whole space: the integrand vanishes off tsupport psi, which is contained in U.

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.IsWeaklyHarmonicOn.mono {d : ℕ} {U V : Set (HCPolySupport.Vec d)} {u : HCPolySupport.Vec d → ℝ} (hu : IsWeaklyHarmonicOn U u) (hVU : V ⊆ U) : IsWeaklyHarmonicOn V u

Weak harmonicity restricts to subsets.

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.IsWeaklyHarmonicOn.euclideanCoordLaplacian_eq_zero {d : ℕ} {U : Set (HCPolySupport.Vec d)} (hU : IsOpen U) {u : HCPolySupport.Vec d → ℝ} (hu : ContDiff ℝ (↑2) u) (hw : IsWeaklyHarmonicOn U u) (x : HCPolySupport.Vec d) : x ∈ U → HCPolySupport.euclideanCoordLaplacian u x = 0

Weak plus C^2 implies classical.

If u is of class C^2 and weakly harmonic on an open set U, then its coordinate Laplacian vanishes at every point of U. Green's identity turns the defining pairing into int (Delta u) psi = 0 for every test function supported in U; the fundamental lemma of the calculus of variations then gives Delta u = 0 almost everywhere on U, and continuity of Delta u upgrades this to every point of the open set U.