WeakDivergence

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

Weak product rule and the divergence-free skew test field

Source: ABK26 (e.sensitivity.basic.split), preparation for the genuine weak integration by parts.

For a smooth compactly supported φ and an a.e. antisymmetric matrix field h with weak first derivatives Dh, the auxiliary vector field t_j := ∑ i (∂_i φ · h_{ij} + φ · ∂_i h_{ij}) (weakly, t_j = ∑ i ∂_i (φ h_{ij}))

is divergence free in the weak sense: it annihilates every smooth compactly supported test gradient. This is the structural mechanism behind the paper's integration by parts ⨍ ∇u · h ∇w = -⨍ u (∇·h) · ∇w, and it isolates the step where antisymmetry of h meets the symmetry of a second derivative.

This module proves:

• integrable_memScalarL2_mul_of_bounded, memScalarL2_bounded_mul — integrability bookkeeping for L² fields against bounded continuous factors on a finite-volume carrier;
• hasWeakPartialDerivOn_smooth_mul — the weak Leibniz rule ∂_i (φ f) = ∂_i φ · f + φ · ∂_i f for smooth compactly supported φ;
• sum_integral_skewTestField_mul_deriv_eq_zero — weak divergence-freeness of the skew test field against smooth compactly supported tests.

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

An L² field times a bounded continuous factor is integrable on a finite-volume carrier.

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.memScalarL2_bounded_mul {d : ℕ} {U : Set (HCPolySupport.Vec d)} {f g : HCPolySupport.Vec d → ℝ} (hf : HCPolySupport.MemScalarL2 U f) (hgc : Continuous g) {C : ℝ} (hgb : ∀ (x : HCPolySupport.Vec d), |g x| ≤ C) : HCPolySupport.MemScalarL2 U fun (x : HCPolySupport.Vec d) => g x * f x

A bounded continuous factor preserves L² membership.

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.exists_abs_bound_of_continuous_of_hasCompactSupport {d : ℕ} {g : HCPolySupport.Vec d → ℝ} (hgc : Continuous g) (hgs : HasCompactSupport g) : ∃ (C : ℝ), ∀ (x : HCPolySupport.Vec d), |g x| ≤ C

Global bound for a continuous compactly supported function.

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.hasWeakPartialDerivOn_smooth_mul {d : ℕ} {U : Set (HCPolySupport.Vec d)} [MeasureTheory.IsFiniteMeasure (HCPolySupport.volumeMeasureOn U)] {i : Fin d} {f fi : HCPolySupport.Vec d → ℝ} (hf2 : HCPolySupport.MemScalarL2 U f) (hfi2 : HCPolySupport.MemScalarL2 U fi) (hf : HCPolySupport.HasWeakPartialDerivOn U i f fi) {φ : HCPolySupport.Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hφc : HasCompactSupport φ) : HCPolySupport.HasWeakPartialDerivOn U i (fun (x : HCPolySupport.Vec d) => φ x * f x) fun (x : HCPolySupport.Vec d) => HCPolySupport.euclideanCoordDeriv i φ x * f x + φ x * fi x

Weak Leibniz rule. If f has weak i-th partial derivative fi on U and φ is smooth and compactly supported, then φ f has weak i-th partial derivative ∂_i φ · f + φ · fi on U.

noncomputable def Algsuperdiff.Section24.Sensitivity.Provider.DhBound.skewTestField {d : ℕ} (h : HCPolySupport.Vec d → HCPolySupport.Mat d) (Dh : Fin d → HCPolySupport.Vec d → HCPolySupport.Mat d) (φ : HCPolySupport.Vec d → ℝ) (x : HCPolySupport.Vec d) : HCPolySupport.Vec d

The skew test field t_j = ∑ i (∂_i φ · h_{ij} + φ · ∂_i h_{ij}) attached to a smooth compactly supported φ and weak derivative data Dh for h.

Equations

• Algsuperdiff.Section24.Sensitivity.Provider.DhBound.skewTestField h Dh φ x j = ∑ i : Fin d, (HCPolySupport.euclideanCoordDeriv i φ x * h x i j + φ x * Dh i x i j)

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.memScalarL2_skewTestField_summand {d : ℕ} {U : Set (HCPolySupport.Vec d)} {h : HCPolySupport.Vec d → HCPolySupport.Mat d} {Dh : Fin d → HCPolySupport.Vec d → HCPolySupport.Mat d} (hmem : ∀ (i j : Fin d), HCPolySupport.MemScalarL2 U fun (x : HCPolySupport.Vec d) => h x i j) (hDmem : ∀ (k i j : Fin d), HCPolySupport.MemScalarL2 U fun (x : HCPolySupport.Vec d) => Dh k x i j) {φ : HCPolySupport.Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hφc : HasCompactSupport φ) (i j : Fin d) : HCPolySupport.MemScalarL2 U fun (x : HCPolySupport.Vec d) => HCPolySupport.euclideanCoordDeriv i φ x * h x i j + φ x * Dh i x i j

Each summand of the skew test field is square integrable.

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.memScalarL2_skewTestField {d : ℕ} {U : Set (HCPolySupport.Vec d)} {h : HCPolySupport.Vec d → HCPolySupport.Mat d} {Dh : Fin d → HCPolySupport.Vec d → HCPolySupport.Mat d} (hmem : ∀ (i j : Fin d), HCPolySupport.MemScalarL2 U fun (x : HCPolySupport.Vec d) => h x i j) (hDmem : ∀ (k i j : Fin d), HCPolySupport.MemScalarL2 U fun (x : HCPolySupport.Vec d) => Dh k x i j) {φ : HCPolySupport.Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hφc : HasCompactSupport φ) (j : Fin d) : HCPolySupport.MemScalarL2 U fun (x : HCPolySupport.Vec d) => skewTestField h Dh φ x j

The skew test field is coordinatewise square integrable.

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.skewTestField_eq_zero_of_notMem_tsupport {d : ℕ} {h : HCPolySupport.Vec d → HCPolySupport.Mat d} {Dh : Fin d → HCPolySupport.Vec d → HCPolySupport.Mat d} {φ : HCPolySupport.Vec d → ℝ} {x : HCPolySupport.Vec d} (hx : x ∉ tsupport φ) : skewTestField h Dh φ x = 0

The skew test field vanishes off the support of φ.

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.sum_integral_skewTestField_mul_deriv_eq_zero {d : ℕ} {U : Set (HCPolySupport.Vec d)} [MeasureTheory.IsFiniteMeasure (HCPolySupport.volumeMeasureOn U)] {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), HCPolySupport.MemScalarL2 U fun (x : HCPolySupport.Vec d) => h x i j) (hDmem : ∀ (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 φ) {ψ : HCPolySupport.Vec d → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) (hψsub : tsupport ψ ⊆ U) : ∑ j : Fin d, ∫ (x : HCPolySupport.Vec d) in U, skewTestField h Dh φ x j * HCPolySupport.euclideanCoordDeriv j ψ x = 0

Weak divergence-freeness of the skew test field. For a.e. antisymmetric h with weak first derivatives Dh, a smooth compactly supported φ with support in U, and every smooth compactly supported test ψ with support in U, ∑ j ∫ t_j ∂_j ψ = 0, t_j = ∑ i (∂_i φ h_{ij} + φ ∂_i h_{ij}).

The proof pairs the weak Leibniz rule with the second-derivative symmetry of ψ, so that the antisymmetry of h cancels the resulting Hessian pairing.