ConstantInvariance

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

Adding a constant to the forcing field does not change the solution

A constant vector field pairs to zero against the gradient of every zero-trace function, so the divergence-form weak equation does not see it. Consequently the localized Dirichlet problem has the same solutions for g and for g + c, and in particular for g and for the centred field x ↦ g x - g y, which has the same 1/2-Hölder seminorm and vanishes at the centre.

The vanishing of the pairing comes from the weak-gradient identity for the constant function 1: tested against a smooth compactly supported function, it says exactly that the integral of a partial derivative vanishes. The passage from smooth test functions to zero-trace ones is the H¹₀ approximating sequence.

References

• ABK26, the localized Dirichlet problems of Section 5.1.

1. The integral of a partial derivative vanishes

theorem Algsuperdiff.Section5.Support.setIntegral_fderiv_eq_zero {d : ℕ} {U : Set (HCPolySupport.Vec d)} (i : Fin d) {psi : HCPolySupport.Vec d → ℝ} (hpsi : ContDiff ℝ (↑⊤) psi) (hsupp : HasCompactSupport psi) (hsub : tsupport psi ⊆ U) : ∫ (x : HCPolySupport.Vec d) in U, (fderiv ℝ psi x) (HCPolySupport.basisVec i) = 0

The integral of a partial derivative of a compactly supported test function vanishes, read off the weak-gradient identity for the constant function 1.

2. The integral of a zero-trace gradient vanishes

theorem Algsuperdiff.Section5.Support.setIntegral_grad_H10_eq_zero {d : ℕ} {U : Set (HCPolySupport.Vec d)} (hUfin : MeasureTheory.volume U ≠ ⊤) (phi : HCPolySupport.H10Function U) (i : Fin d) : ∫ (x : HCPolySupport.Vec d) in U, phi.grad x i = 0

theorem Algsuperdiff.Section5.Support.setIntegral_vecDot_const_H10_eq_zero {d : ℕ} {U : Set (HCPolySupport.Vec d)} (hUfin : MeasureTheory.volume U ≠ ⊤) (phi : HCPolySupport.H10Function U) (c : HCPolySupport.Vec d) : ∫ (x : HCPolySupport.Vec d) in U, HCPolySupport.vecDot c (phi.grad x) = 0

3. The equation does not see a constant forcing field

theorem Algsuperdiff.Section5.Support.isDivFormWeakSolutionOn_add_const {d : ℕ} {W : Set (HCPolySupport.Vec d)} (hWfin : MeasureTheory.volume W ≠ ⊤) {a : HCPolySupport.CoeffField d} {u : HCPolySupport.H1Function W} {g : HCPolySupport.Vec d → HCPolySupport.Vec d} (hgL2 : HCPolySupport.MemVectorL2 W g) (c : HCPolySupport.Vec d) (h : Section4.Support.IsDivFormWeakSolutionOn a W u g) : Section4.Support.IsDivFormWeakSolutionOn a W u fun (x : HCPolySupport.Vec d) => g x + c

theorem Algsuperdiff.Section5.Support.isDirichletSolutionAt_add_const {d : ℕ} {y : HCPolySupport.Vec d} {n : ℤ} {a : HCPolySupport.CoeffField d} {u : HCPolySupport.H1Function (cubeSetAt y n)} {g : HCPolySupport.Vec d → HCPolySupport.Vec d} (hgL2 : HCPolySupport.MemVectorL2 (cubeSetAt y n) g) (c : HCPolySupport.Vec d) (h : IsDirichletSolutionAt a y n u g) : IsDirichletSolutionAt a y n u fun (x : HCPolySupport.Vec d) => g x + c

Adding a constant to the forcing field leaves the solutions unchanged.

theorem Algsuperdiff.Section5.Support.isDirichletSolutionAt_sub_const {d : ℕ} {y : HCPolySupport.Vec d} {n : ℤ} {a : HCPolySupport.CoeffField d} {u : HCPolySupport.H1Function (cubeSetAt y n)} {g : HCPolySupport.Vec d → HCPolySupport.Vec d} (hgL2 : HCPolySupport.MemVectorL2 (cubeSetAt y n) g) (c : HCPolySupport.Vec d) (h : IsDirichletSolutionAt a y n u g) : IsDirichletSolutionAt a y n u fun (x : HCPolySupport.Vec d) => g x - c

Centring the forcing field at the centre of the cube leaves the solutions unchanged.