WeakIBP

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

The genuine weak integration by parts for the D_h splitting

Source: ABK26 (e.sensitivity.basic.split), second step. For an a.e. antisymmetric matrix field h with essentially bounded weak first derivatives and every u ∈ H¹₀(U), w ∈ H¹(U), ∫ ∇u · h ∇w = -∫ u (∇·h) · ∇w, (∇·h)_j = ∑ i ∂_i h_{ij}.

This is the genuine weak integration by parts of the splitting identity: it requires the test combination to lie in H¹₀ (zero trace), in contrast to the purely algebraic skew cancellation in SkewCancellation.lean. The proof first establishes the identity for smooth compactly supported tests through the divergence-free pairing lemma (integral_euclideanGradient_dot_matVecMul_grad_eq_neg), then closes it under the H¹₀ approximation package (integral_grad_dot_matVecMul_grad_eq_neg_of_hasWeakDeriv).

def Algsuperdiff.Section24.Sensitivity.Provider.DhBound.matWeakDiv {d : ℕ} (Dh : Fin d → HCPolySupport.Vec d → HCPolySupport.Mat d) (x : HCPolySupport.Vec d) : HCPolySupport.Vec d

The weak column divergence (∇·h)_j = ∑ i ∂_i h_{ij} assembled from first-derivative data Dh k x i j = ∂_k h_{ij} (x).

Equations

• Algsuperdiff.Section24.Sensitivity.Provider.DhBound.matWeakDiv Dh x j = ∑ i : Fin d, Dh i x i j

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.memScalarL2_of_continuous_of_bounded {d : ℕ} {U : Set (HCPolySupport.Vec d)} [MeasureTheory.IsFiniteMeasure (HCPolySupport.volumeMeasureOn U)] {g : HCPolySupport.Vec d → ℝ} (hgc : Continuous g) {C : ℝ} (hgb : ∀ (x : HCPolySupport.Vec d), |g x| ≤ C) : HCPolySupport.MemScalarL2 U g

Bounded continuous functions are square integrable on a finite-volume carrier.

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.vecDot_matWeakDiv_eq_sum {d : ℕ} {Dh : Fin d → HCPolySupport.Vec d → HCPolySupport.Mat d} {g : HCPolySupport.Vec d → HCPolySupport.Vec d} : (fun (x : HCPolySupport.Vec d) => HCPolySupport.vecDot (matWeakDiv Dh x) (g x)) = fun (x : HCPolySupport.Vec d) => ∑ j : Fin d, ∑ i : Fin d, Dh i x i j * g x j

The weak-divergence pairing x ↦ (∇·h)(x) · g(x) expanded as a double sum.

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.integrable_vecDot_matWeakDiv {d : ℕ} {U : Set (HCPolySupport.Vec d)} {Dh : Fin d → HCPolySupport.Vec d → HCPolySupport.Mat d} (hDmem2 : ∀ (k i j : Fin d), HCPolySupport.MemScalarL2 U fun (x : HCPolySupport.Vec d) => Dh k x i j) {g : HCPolySupport.Vec d → HCPolySupport.Vec d} (hg : ∀ (j : Fin d), HCPolySupport.MemScalarL2 U fun (x : HCPolySupport.Vec d) => g x j) : MeasureTheory.Integrable (fun (x : HCPolySupport.Vec d) => HCPolySupport.vecDot (matWeakDiv Dh x) (g x)) (HCPolySupport.volumeMeasureOn U)

The weak-divergence pairing against an L² gradient is integrable from square-integrable derivative data.

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.memScalarL2_vecDot_matWeakDiv {d : ℕ} {U : Set (HCPolySupport.Vec d)} {Dh : Fin d → HCPolySupport.Vec d → HCPolySupport.Mat d} (hDmem : ∀ (k i j : Fin d), MeasureTheory.MemLp (fun (x : HCPolySupport.Vec d) => Dh k x i j) ⊤ (HCPolySupport.volumeMeasureOn U)) {g : HCPolySupport.Vec d → HCPolySupport.Vec d} (hg : ∀ (j : Fin d), HCPolySupport.MemScalarL2 U fun (x : HCPolySupport.Vec d) => g x j) : HCPolySupport.MemScalarL2 U fun (x : HCPolySupport.Vec d) => HCPolySupport.vecDot (matWeakDiv Dh x) (g x)

The weak-divergence pairing is square integrable when the derivative data is essentially bounded.

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.memScalarL2_matVecMul_coord {d : ℕ} {U : Set (HCPolySupport.Vec d)} {h : HCPolySupport.Vec d → HCPolySupport.Mat d} (hmem : ∀ (i j : Fin d), MeasureTheory.MemLp (fun (x : HCPolySupport.Vec d) => h x i j) ⊤ (HCPolySupport.volumeMeasureOn U)) {g : HCPolySupport.Vec d → HCPolySupport.Vec d} (hg : ∀ (j : Fin d), HCPolySupport.MemScalarL2 U fun (x : HCPolySupport.Vec d) => g x j) (i : Fin d) : HCPolySupport.MemScalarL2 U fun (x : HCPolySupport.Vec d) => HCPolySupport.matVecMul (h x) (g x) i

Coordinates of the skew-multiplied gradient are square integrable when the matrix entries are essentially bounded.

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.integral_euclideanGradient_dot_matVecMul_grad_eq_neg {d : ℕ} {U : Set (HCPolySupport.Vec d)} (hU : HCPolySupport.IsOpenBoundedConvexDomain U) (hUne : U.Nonempty) {h : HCPolySupport.Vec d → HCPolySupport.Mat d} {Dh : Fin d → HCPolySupport.Vec d → HCPolySupport.Mat d} (hskew : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn U, HCPolySupport.symmPart (h x) = 0) (hmem2 : ∀ (i j : Fin d), HCPolySupport.MemScalarL2 U fun (x : HCPolySupport.Vec d) => h x i j) (hDmem2 : ∀ (k i j : Fin d), HCPolySupport.MemScalarL2 U fun (x : HCPolySupport.Vec d) => Dh k x i j) (hweak : ∀ (k i j : Fin d), HCPolySupport.HasWeakPartialDerivOn U k (fun (x : HCPolySupport.Vec d) => h x i j) fun (x : HCPolySupport.Vec d) => Dh k x i j) {φ : HCPolySupport.Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hφc : HasCompactSupport φ) (hφsub : tsupport φ ⊆ U) (w : HCPolySupport.H1Function U) : ∫ (x : HCPolySupport.Vec d) in U, HCPolySupport.vecDot (HCPolySupport.euclideanGradient φ x) (HCPolySupport.matVecMul (h x) (w.grad x)) = -∫ (x : HCPolySupport.Vec d) in U, φ x * HCPolySupport.vecDot (matWeakDiv Dh x) (w.grad x)

Weak integration by parts at a smooth compactly supported test. For a.e. antisymmetric h with square-integrable weak first derivatives and every smooth compactly supported φ with support in U, ∫ ∇φ · h ∇w = -∫ φ (∇·h) · ∇w.

Only L² control of h and Dh is used at this stage.

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.integral_grad_dot_matVecMul_grad_eq_neg_of_hasWeakDeriv {d : ℕ} {U : Set (HCPolySupport.Vec d)} (hU : HCPolySupport.IsOpenBoundedConvexDomain U) (hUne : U.Nonempty) {h : HCPolySupport.Vec d → HCPolySupport.Mat d} {Dh : Fin d → HCPolySupport.Vec d → HCPolySupport.Mat d} (hskew : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn U, HCPolySupport.symmPart (h x) = 0) (hmem : ∀ (i j : Fin d), MeasureTheory.MemLp (fun (x : HCPolySupport.Vec d) => h x i j) ⊤ (HCPolySupport.volumeMeasureOn U)) (hDmem : ∀ (k i j : Fin d), MeasureTheory.MemLp (fun (x : HCPolySupport.Vec d) => Dh k x i j) ⊤ (HCPolySupport.volumeMeasureOn U)) (hweak : ∀ (k i j : Fin d), HCPolySupport.HasWeakPartialDerivOn U k (fun (x : HCPolySupport.Vec d) => h x i j) fun (x : HCPolySupport.Vec d) => Dh k x i j) (u : HCPolySupport.H10Function U) (w : HCPolySupport.H1Function U) : ∫ (x : HCPolySupport.Vec d) in U, HCPolySupport.vecDot (u.grad x) (HCPolySupport.matVecMul (h x) (w.grad x)) = -∫ (x : HCPolySupport.Vec d) in U, u.toFun x * HCPolySupport.vecDot (matWeakDiv Dh x) (w.grad x)

The genuine weak integration by parts for the D_h splitting. For an a.e. antisymmetric matrix field h with essentially bounded entries and essentially bounded weak first derivatives Dh, every u ∈ H¹₀(U) and every w ∈ H¹(U) on an open bounded convex carrier satisfy ∫ ∇u · h ∇w = -∫ u (∇·h) · ∇w.

The zero-trace hypothesis on u is the exact structural input demanded by the source display e.sensitivity.basic.split; the response combination w + w* + ℓ_p is inserted here once its H¹₀ membership is provided.