SplitIdentity

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

The D_h splitting identity e.sensitivity.basic.split

Source: ABK26. With w = ½ v(·, U, p, q; a) and w* = ½ v(·, U, p, -q; aᵗ), ⨍ ∇w* · h ∇w = -p · ⨍ h ∇w - ⨍ (w + w* + ℓ_p) (∇·h) · ∇w.

The two ingredients are already proved upstream: the pointwise skew cancellation (quadForm_coarseMatrixDerivative_eq_average_sum_pairing) and the weak integration by parts (integral_grad_dot_matVecMul_grad_eq_neg_of_hasWeakDeriv). What this module adds is the bookkeeping that turns the two into a single identity for the frozen quadratic form at the unscaled maximizers vAdj, v, namely P · D_h P = -2 p · ⨍ h ∇v - 2 ⨍ u (∇·h) · ∇v,

where u ∈ H¹₀(U) is any zero-trace witness for the source combination ½(∇vAdj + ∇v) + p = ∇w + ∇w* + p.

The identity is proved at a general Chapter 2 domain U with a general L∞ skew field and general essentially bounded weak first-derivative data; the frozen unit-cube carrier is a specialization at the end of the file.

Integrability of the two pairings

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Assembly.memScalarL2_matVecMul_grad {d : ℕ} {U : HCPolySupport.Book.Ch02.Domain d} (h : Frozen.Section24.LInfSkewMatrixFieldOn U) (v : HCPolySupport.H1Function U.carrier) (i : Fin d) : HCPolySupport.MemScalarL2 U.carrier fun (x : HCPolySupport.Vec d) => HCPolySupport.matVecMul (↑↑h x) (v.grad x) i

Coordinates of h ∇v are square integrable.

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Assembly.integrable_vecDot_matVecMul_grad {d : ℕ} {U : HCPolySupport.Book.Ch02.Domain d} (h : Frozen.Section24.LInfSkewMatrixFieldOn U) (u v : HCPolySupport.H1Function U.carrier) : MeasureTheory.Integrable (fun (x : HCPolySupport.Vec d) => HCPolySupport.vecDot (u.grad x) (HCPolySupport.matVecMul (↑↑h x) (v.grad x))) (HCPolySupport.volumeMeasureOn U.carrier)

The ∇u · h ∇v integrand is integrable.

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Assembly.integrable_vecDot_const_matVecMul_grad {d : ℕ} {U : HCPolySupport.Book.Ch02.Domain d} (h : Frozen.Section24.LInfSkewMatrixFieldOn U) (v : HCPolySupport.H1Function U.carrier) (p : HCPolySupport.Vec d) : MeasureTheory.Integrable (fun (x : HCPolySupport.Vec d) => HCPolySupport.vecDot p (HCPolySupport.matVecMul (↑↑h x) (v.grad x))) (HCPolySupport.volumeMeasureOn U.carrier)

The p · h ∇v integrand is integrable.

Average-level bookkeeping

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Assembly.average_vecDot_const_eq_vecDot_averageVec {d : ℕ} {U : HCPolySupport.Book.Ch02.Domain d} {G : HCPolySupport.Vec d → HCPolySupport.Vec d} (hG : ∀ (i : Fin d), MeasureTheory.Integrable (fun (x : HCPolySupport.Vec d) => G x i) (HCPolySupport.volumeMeasureOn U.carrier)) (p : HCPolySupport.Vec d) : (HCPolySupport.Book.Ch02.average U fun (x : HCPolySupport.Vec d) => HCPolySupport.vecDot p (G x)) = HCPolySupport.vecDot p (HCPolySupport.Book.Ch02.averageVec U G)

Pulling a constant vector out of the average.

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Assembly.average_sub {d : ℕ} {U : HCPolySupport.Book.Ch02.Domain d} {f g : HCPolySupport.Vec d → ℝ} (hf : MeasureTheory.Integrable f (HCPolySupport.volumeMeasureOn U.carrier)) (hg : MeasureTheory.Integrable g (HCPolySupport.volumeMeasureOn U.carrier)) : (HCPolySupport.Book.Ch02.average U fun (x : HCPolySupport.Vec d) => f x - g x) = HCPolySupport.Book.Ch02.average U f - HCPolySupport.Book.Ch02.average U g

Averages are additive on integrable summands.

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Assembly.average_const_mul {d : ℕ} {U : HCPolySupport.Book.Ch02.Domain d} (c : ℝ) (f : HCPolySupport.Vec d → ℝ) : (HCPolySupport.Book.Ch02.average U fun (x : HCPolySupport.Vec d) => c * f x) = c * HCPolySupport.Book.Ch02.average U f

Averages commute with multiplication by a real constant.

The splitting identity

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Assembly.quadForm_coarseMatrixDerivative_eq_split {d : ℕ} (U : HCPolySupport.Book.Ch02.Domain d) (a : HCPolySupport.Book.Ch02.CoeffOn U) (h : Frozen.Section24.LInfSkewMatrixFieldOn U) {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.carrier)) (hweak : ∀ (k i j : Fin d), HCPolySupport.HasWeakPartialDerivOn U.carrier k (fun (x : HCPolySupport.Vec d) => ↑↑h x i j) fun (x : HCPolySupport.Vec d) => Dh k x i j) (p q : HCPolySupport.Vec d) (vAdj : HCPolySupport.Book.Ch02.Solution U a.transpose) (v : HCPolySupport.Book.Ch02.Solution U a) (hvAdj : HCPolySupport.Book.Ch02.IsResponseMaximizer U a.transpose p (-q) vAdj) (hv : HCPolySupport.Book.Ch02.IsResponseMaximizer U a p q v) (u : HCPolySupport.H10Function U.carrier) (hu : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn U.carrier, u.grad x = 2⁻¹ • (vAdj.toH1.grad x + v.toH1.grad x) + p) : HCPolySupport.blockVecDot (p, -q) (HCPolySupport.blockMatVecMul (Frozen.Section24.coarseMatrixDerivative U a ↑h) (p, -q)) = -2 * HCPolySupport.vecDot p (HCPolySupport.Book.Ch02.averageVec U fun (x : HCPolySupport.Vec d) => HCPolySupport.matVecMul (↑↑h x) (v.toH1.grad x)) - 2 * HCPolySupport.Book.Ch02.average U fun (x : HCPolySupport.Vec d) => u.toFun x * HCPolySupport.vecDot (matWeakDiv Dh x) (v.toH1.grad x)

The D_h splitting identity at a general domain.

P · D_h(U; a) P = -2 p · ⨍_U h ∇v - 2 ⨍_U u (∇·h) · ∇v,

for P = (p, -q), arbitrary response maximizers vAdj (for (aᵗ, p, -q)) and v (for (a, p, q)), and any H¹₀(U) witness u for the source combination ½(∇vAdj + ∇v) + p.

The u-hypothesis is exactly the source claim ∇w + ∇w* + p ∈ L²_{pot,0}(U); it is discharged at every use.

The frozen unit-cube carrier

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Assembly.quadForm_coarseMatrixDerivative_unitCube_eq_split {d : ℕ} (a : HCPolySupport.Book.Ch02.CoeffOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0))) (h : Frozen.Section24.UnitCubeSkewW2Infinity d) (p q : HCPolySupport.Vec d) (vAdj : HCPolySupport.Book.Ch02.Solution (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0)) a.transpose) (v : HCPolySupport.Book.Ch02.Solution (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0)) a) (hvAdj : HCPolySupport.Book.Ch02.IsResponseMaximizer (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0)) a.transpose p (-q) vAdj) (hv : HCPolySupport.Book.Ch02.IsResponseMaximizer (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0)) a p q v) (u : HCPolySupport.H10Function (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0)).carrier) (hu : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0)).carrier, u.grad x = 2⁻¹ • (vAdj.toH1.grad x + v.toH1.grad x) + p) : HCPolySupport.blockVecDot (p, -q) (HCPolySupport.blockMatVecMul (Frozen.Section24.coarseMatrixDerivative (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0)) a ↑h.toLInfSkewMatrixFieldOn) (p, -q)) = -2 * HCPolySupport.vecDot p (HCPolySupport.Book.Ch02.averageVec (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0)) fun (x : HCPolySupport.Vec d) => HCPolySupport.matVecMul (↑↑h.toLInfSkewMatrixFieldOn x) (v.toH1.grad x)) - 2 * HCPolySupport.Book.Ch02.average (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0)) fun (x : HCPolySupport.Vec d) => u.toFun x * HCPolySupport.vecDot (matWeakDiv (unitCubeDerivData h) x) (v.toH1.grad x)

The D_h splitting identity at the frozen unit-cube carrier. All analytic premises are discharged by the frozen UnitCubeSkewW2Infinity structure fields; the only remaining input is the H¹₀ witness.