FieldDivergenceTest

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

Integrating a C¹ vector field by parts against a zero-trace Sobolev function

Two of the Section 5.2 computations pair a classical vector field with the gradient of a Sobolev function of zero trace: the datum g(x) = x_1 e_1, whose divergence is the constant 1, and the gradient of a smooth barrier, whose divergence is its Laplacian. Both are instances of one identity,

  ∫_U F · ∇φ = - ∫_U (∇·F) φ ,   F ∈ C¹ ,  φ ∈ H¹₀(U) ,

on a bounded measurable set U. Against a smooth compactly supported test function the identity is the defining property of the weak partial derivatives of the components of F; the passage to a zero-trace Sobolev test function is the L² limit along the approximating sequence carried by H¹₀.

Main definitions

• matFieldDiv k — the matrix-field divergence, contracting its first index.
• vecFieldDiv F — the divergence (∇·F)(x) = ∑_i ∂_i F_i(x) of a vector field, contracting the index of the field against the direction of differentiation.

Main results

• integral_vecDot_h10Grad_eq_neg_integral_vecFieldDiv_mul — the identity above.

References

• ABK26, the exit-time comparison of Section 5.2.

noncomputable def Algsuperdiff.Section5.Support.matFieldDiv {d : ℕ} (k : HCPolySupport.Vec d → HCPolySupport.Mat d) : HCPolySupport.Vec d → HCPolySupport.Vec d

The divergence of a matrix field, contracting the first index:

  (∇ · k)_j (x) = ∑_i ∂_i k_{i j}(x) .

This is the contraction that sends a ∇u to ∇ · a ∇u, and the one under which the manuscript's antisymmetry display has the printed signs.

Equations

• Algsuperdiff.Section5.Support.matFieldDiv k x j = ∑ i : Fin d, HCPolySupport.euclideanCoordDeriv i (fun (y : HCPolySupport.Vec d) => k y i j) x

theorem Algsuperdiff.Section5.Support.matFieldDiv_apply {d : ℕ} (k : HCPolySupport.Vec d → HCPolySupport.Mat d) (x : HCPolySupport.Vec d) (j : Fin d) : matFieldDiv k x j = ∑ i : Fin d, HCPolySupport.euclideanCoordDeriv i (fun (y : HCPolySupport.Vec d) => k y i j) x

The defining coordinate formula of matFieldDiv.

theorem Algsuperdiff.Section5.Support.continuous_matFieldDiv_apply {d : ℕ} {k : HCPolySupport.Vec d → HCPolySupport.Mat d} (hk : ∀ (a b : Fin d), ContDiff ℝ 1 fun (x : HCPolySupport.Vec d) => k x a b) (j : Fin d) : Continuous fun (x : HCPolySupport.Vec d) => matFieldDiv k x j

Each coordinate of the divergence of a C¹ matrix field is continuous.

noncomputable def Algsuperdiff.Section5.Support.vecFieldDiv {d : ℕ} (F : HCPolySupport.Vec d → HCPolySupport.Vec d) : HCPolySupport.Vec d → ℝ

The divergence of a vector field, (∇·F)(x) = ∑_i ∂_i F_i(x).

Equations

• Algsuperdiff.Section5.Support.vecFieldDiv F x = ∑ i : Fin d, (fderiv ℝ (fun (z : HCPolySupport.Vec d) => F z i) x) (HCPolySupport.basisVec i)

theorem Algsuperdiff.Section5.Support.vecFieldDiv_apply {d : ℕ} (F : HCPolySupport.Vec d → HCPolySupport.Vec d) (x : HCPolySupport.Vec d) : vecFieldDiv F x = ∑ i : Fin d, (fderiv ℝ (fun (z : HCPolySupport.Vec d) => F z i) x) (HCPolySupport.basisVec i)

1. Square integrability on a bounded set

theorem Algsuperdiff.Section5.Support.exists_bound_of_continuous {d : ℕ} {U : Set (HCPolySupport.Vec d)} (hU : HCPolySupport.IsBoundedDomain U) {f : HCPolySupport.Vec d → ℝ} (hf : Continuous f) : ∃ (C : ℝ), ∀ x ∈ U, |f x| ≤ C

A continuous function is bounded on a bounded domain.

theorem Algsuperdiff.Section5.Support.memScalarL2_mul_of_continuous_left {d : ℕ} {U : Set (HCPolySupport.Vec d)} (hUm : MeasurableSet U) (hUb : HCPolySupport.IsBoundedDomain U) {g f : HCPolySupport.Vec d → ℝ} (hg : Continuous g) (hf : HCPolySupport.MemScalarL2 U f) : HCPolySupport.MemScalarL2 U fun (x : HCPolySupport.Vec d) => g x * f x

Multiplication by a continuous function preserves L² on a bounded measurable domain.

theorem Algsuperdiff.Section5.Support.memScalarL2_mul_of_continuous_right {d : ℕ} {U : Set (HCPolySupport.Vec d)} (hUm : MeasurableSet U) (hUb : HCPolySupport.IsBoundedDomain U) {f g : HCPolySupport.Vec d → ℝ} (hf : HCPolySupport.MemScalarL2 U f) (hg : Continuous g) : HCPolySupport.MemScalarL2 U fun (x : HCPolySupport.Vec d) => f x * g x

Right multiplication by a continuous function preserves L² on a bounded measurable domain.

theorem Algsuperdiff.Section5.Support.memScalarL2_of_continuous_of_isBoundedDomain {d : ℕ} {U : Set (HCPolySupport.Vec d)} (hUm : MeasurableSet U) (hU : HCPolySupport.IsBoundedDomain U) {f : HCPolySupport.Vec d → ℝ} (hf : Continuous f) : HCPolySupport.MemScalarL2 U f

A continuous function is square integrable on a bounded measurable set.

theorem Algsuperdiff.Section5.Support.memScalarL2_of_continuous_hasCompactSupport {d : ℕ} {U : Set (HCPolySupport.Vec d)} {f : HCPolySupport.Vec d → ℝ} (hf : Continuous f) (hfc : HasCompactSupport f) : HCPolySupport.MemScalarL2 U f

A continuous compactly supported function is square integrable on any set.

theorem Algsuperdiff.Section5.Support.integrable_mul_of_memScalarL2 {d : ℕ} {U : Set (HCPolySupport.Vec d)} {f g : HCPolySupport.Vec d → ℝ} (hf : HCPolySupport.MemScalarL2 U f) (hg : HCPolySupport.MemScalarL2 U g) : MeasureTheory.Integrable (fun (x : HCPolySupport.Vec d) => f x * g x) (MeasureTheory.volume.restrict U)

The product of two square-integrable scalar fields is integrable.

theorem Algsuperdiff.Section5.Support.integral_vecDot_eq_sum_coord {d : ℕ} {U : Set (HCPolySupport.Vec d)} {P G : HCPolySupport.Vec d → HCPolySupport.Vec d} (hP : ∀ (i : Fin d), HCPolySupport.MemScalarL2 U fun (x : HCPolySupport.Vec d) => P x i) (hG : ∀ (i : Fin d), HCPolySupport.MemScalarL2 U fun (x : HCPolySupport.Vec d) => G x i) : ∫ (x : HCPolySupport.Vec d) in U, HCPolySupport.vecDot (P x) (G x) = ∑ i : Fin d, ∫ (x : HCPolySupport.Vec d) in U, P x i * G x i

The integral of an L² dot product is the sum of its coordinate integrals.

2. The integration by parts

theorem Algsuperdiff.Section5.Support.integral_vecDot_h10Grad_eq_neg_integral_vecFieldDiv_mul {d : ℕ} {U : Set (HCPolySupport.Vec d)} (hUm : MeasurableSet U) (hU : HCPolySupport.IsBoundedDomain U) {F : HCPolySupport.Vec d → HCPolySupport.Vec d} (hF : ∀ (i : Fin d), ContDiff ℝ 1 fun (z : HCPolySupport.Vec d) => F z i) (phi : HCPolySupport.H10Function U) : ∫ (x : HCPolySupport.Vec d) in U, HCPolySupport.vecDot (F x) (phi.grad x) = -∫ (x : HCPolySupport.Vec d) in U, vecFieldDiv F x * phi.toFun x

A C¹ vector field integrates by parts against a zero-trace Sobolev function: ∫_U F·∇φ = -∫_U (∇·F) φ.