BoundaryWeakTests

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

Smooth tests for the divergence-form equation with a scalar source

The zeroth-order weak equation is stated against the bundled H¹₀ carrier. Two conversions are used repeatedly by the reflection argument: smooth compactly supported tests already determine the equation, and a smooth competitor which happens to lie in H¹₀ may be tested with its classical gradient. Both are the coefficient-carrying analogues of the corresponding harmonicity conversions.

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Freezing.integral_vecDot_split_coords {d : ℕ} {W : Set (HCPolySupport.Vec d)} (F G : HCPolySupport.Vec d → HCPolySupport.Vec d) (hF : ∀ (j : Fin d), MeasureTheory.MemLp (fun (y : HCPolySupport.Vec d) => F y j) 2 (MeasureTheory.volume.restrict W)) (hG : ∀ (j : Fin d), MeasureTheory.MemLp (fun (y : HCPolySupport.Vec d) => G y j) 2 (MeasureTheory.volume.restrict W)) : ∫ (y : HCPolySupport.Vec d) in W, HCPolySupport.vecDot (F y) (G y) = ∑ j : Fin d, ∫ (y : HCPolySupport.Vec d) in W, G y j * F y j

The tested pairing splits into its d coordinate products.

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Freezing.memLp_two_of_contDiff_restrict {d : ℕ} {W : Set (HCPolySupport.Vec d)} {f : HCPolySupport.Vec d → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hfc : HasCompactSupport f) : MeasureTheory.MemLp f 2 (MeasureTheory.volume.restrict W)

A smooth compactly supported function is square integrable on every window.

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Freezing.isMatrixDivFormWeakSolutionZerothOrderOn_of_contDiff_tests {d : ℕ} {W : Set (HCPolySupport.Vec d)} {a : HCPolySupport.CoeffField d} {u : HCPolySupport.H1Function W} {g : HCPolySupport.Vec d → ℝ} (hflux : ∀ (j : Fin d), MeasureTheory.MemLp (fun (y : HCPolySupport.Vec d) => HCPolySupport.matVecMul (a y) (u.grad y) j) 2 (MeasureTheory.volume.restrict W)) (hg : MeasureTheory.MemLp g 2 (MeasureTheory.volume.restrict W)) (htest : ∀ (φ : HCPolySupport.Vec d → ℝ), ContDiff ℝ (↑⊤) φ → HasCompactSupport φ → tsupport φ ⊆ W → ∫ (y : HCPolySupport.Vec d) in W, HCPolySupport.vecDot (HCPolySupport.matVecMul (a y) (u.grad y)) (HCPolySupport.euclideanGradient φ y) = ∫ (y : HCPolySupport.Vec d) in W, g y * φ y) : Ported.IsMatrixDivFormWeakSolutionZerothOrderOn a W u g 0

Smooth tests suffice for the divergence-form equation with a bounded scalar source. The proof tests against the H¹₀ package's own smooth approximants and passes to the limit coordinatewise, using the L² convergence of both values and gradients.

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Freezing.integral_pairing_eq_of_memH10 {d : ℕ} {W : Set (HCPolySupport.Vec d)} (hWopen : IsOpen W) [MeasureTheory.IsFiniteMeasure (MeasureTheory.volume.restrict W)] {a : HCPolySupport.CoeffField d} {u : HCPolySupport.H1Function W} {g : HCPolySupport.Vec d → ℝ} (hu : Ported.IsMatrixDivFormWeakSolutionZerothOrderOn a W u g 0) {ψ : HCPolySupport.Vec d → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hmem : HCPolySupport.MemH10 W ψ) : ∫ (y : HCPolySupport.Vec d) in W, HCPolySupport.vecDot (HCPolySupport.matVecMul (a y) (u.grad y)) (HCPolySupport.euclideanGradient ψ y) = ∫ (y : HCPolySupport.Vec d) in W, g y * ψ y

A smooth H¹₀ competitor may be tested with its classical gradient. The H10Function witness carries some weak gradient of the competitor; on the open window it agrees almost everywhere with the classical one.