ScalarToDivergence

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

Smooth scalar forcing as divergence forcing

A globally C¹ scalar field is converted into divergence forcing by placing the negative of its one-coordinate primitive in one vector coordinate. The resulting field is in L² on a bounded convex domain and has exactly the weak pairing required by the literal divergence-right-hand-side predicate.

This module does not extend the construction to nonsmooth or merely almost everywhere bounded scalar forcing.

noncomputable def DivergenceFormProcess.coordinatePrimitiveH1 {d : ℕ} {U : Set (HCPolySupport.Vec d)} (hU : HCPolySupport.IsOpenBoundedConvexDomain U) (q : HCPolySupport.Vec d → ℝ) (hq : ContDiff ℝ 1 q) (i : Fin d) (z : ℝ) : HCPolySupport.H1Function U

The coordinate primitive packaged as an H¹ function on a bounded convex domain.

Equations

• DivergenceFormProcess.coordinatePrimitiveH1 hU q hq i z = HCPolySupport.H1Function.ofContDiffOnIsOpenBoundedConvexDomain hU ⋯

noncomputable def DivergenceFormProcess.scalarToDivergenceField {d : ℕ} (q : HCPolySupport.Vec d → ℝ) (i : Fin d) (z : ℝ) : HCPolySupport.Vec d → HCPolySupport.Vec d

The divergence field with selected coordinate equal to the negative coordinate primitive and every other coordinate equal to zero.

Equations

• DivergenceFormProcess.scalarToDivergenceField q i z x j = if j = i then -DivergenceFormProcess.coordinatePrimitive q i z x else 0

theorem DivergenceFormProcess.coordinatePrimitiveH1_grad_selected {d : ℕ} {U : Set (HCPolySupport.Vec d)} (hU : HCPolySupport.IsOpenBoundedConvexDomain U) (q : HCPolySupport.Vec d → ℝ) (hq : ContDiff ℝ 1 q) (i : Fin d) (z : ℝ) (x : HCPolySupport.Vec d) : (coordinatePrimitiveH1 hU q hq i z).grad x i = q x

The selected weak-gradient coordinate of the packaged primitive is the original scalar field.

theorem DivergenceFormProcess.scalarToDivergenceField_memVectorL2 {d : ℕ} {U : Set (HCPolySupport.Vec d)} (hU : HCPolySupport.IsOpenBoundedConvexDomain U) (q : HCPolySupport.Vec d → ℝ) (hq : ContDiff ℝ 1 q) (i : Fin d) (z : ℝ) : HCPolySupport.MemVectorL2 U (scalarToDivergenceField q i z)

The smooth scalar-to-divergence field belongs to vector L² on the bounded domain.

theorem DivergenceFormProcess.integral_scalarToDivergenceField_vecDot_grad_eq {d : ℕ} {U : Set (HCPolySupport.Vec d)} (hU : HCPolySupport.IsOpenBoundedConvexDomain U) (q : HCPolySupport.Vec d → ℝ) (hq : ContDiff ℝ 1 q) (i : Fin d) (z : ℝ) (φ : HCPolySupport.H10Function U) : ∫ (x : HCPolySupport.Vec d) in U, HCPolySupport.vecDot (scalarToDivergenceField q i z x) (φ.grad x) = ∫ (x : HCPolySupport.Vec d) in U, q x * φ.toFun x

The divergence field pairs with every zero-trace test exactly as the original scalar forcing.