Coarse-graining support:

Support.Sobolev.Foundations.CubeNeumannW22CZ.WeakInteriorDQ.IntegralIdentity

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

theorem HCPolySupport.WeakPoissonEquationOn.test_backwardDifferenceQuotient_sqCutoffForwardDifferenceQuotient_gradientSplit {d : ℕ} {U V : Set (Vec d)} {u : H1Function U} {f : Vec d → ℝ} (h : WeakPoissonEquationOn U u f) (hU : IsOpen U) (hf : MemScalarL2 U f) (hV : IsOpenBoundedConvexDomain V) (hVU : V ⊆ U) (step : ℝ) (i : Fin d) (hVshift : V ⊆ translateSet (-step • basisVec i) U) {η : Vec d → ℝ} (hη : ContDiff ℝ (↑⊤) η) (hη_compact : HasCompactSupport η) (hη_sub : tsupport η ⊆ V) : ∫ (x : Vec d) in U, vecDot (u.grad x) (step⁻¹ • ((localizedSqCutoffForwardDifferenceQuotientToAmbient u hV hVU step i hVshift hη hη_compact hη_sub).grad x - (localizedSqShiftedCutoffBackwardDifferenceQuotientToAmbient u hV hVU step i hVshift hη hη_compact hη_sub).grad x)) = ∫ (x : Vec d) in U, f x * euclideanBackwardDifferenceQuotient step i (fun (y : Vec d) => η y ^ 2 * euclideanForwardDifferenceQuotient step i u.toFun y) x

The same direct-test identity with the explicit ambient gradient expanded as the difference of the unshifted and shifted localized gradients.

theorem HCPolySupport.WeakPoissonEquationOn.integral_dot_backwardDifference_cutoffForwardDifference_grad_eq_sub_integrals_on {d : ℕ} {U V : Set (Vec d)} {G : Vec d → Vec d} (hG : MemVectorL2 U G) (u : H1Function U) (hV : IsOpenBoundedConvexDomain V) (hVU : V ⊆ U) (step : ℝ) (i : Fin d) (hVshift : V ⊆ translateSet (-step • basisVec i) U) {η : Vec d → ℝ} (hη : ContDiff ℝ (↑⊤) η) (hη_compact : HasCompactSupport η) (hη_sub : tsupport η ⊆ V) : ∫ (x : Vec d) in U, vecDot (G x) ((backwardDifferenceQuotientSqCutoffForwardDifferenceQuotientToAmbient u hV hVU step i hVshift hη hη_compact hη_sub).grad x) = step⁻¹ * ((∫ (x : Vec d) in V, vecDot (G x) ((localizedSqCutoffForwardDifferenceQuotientToAmbient u hV hVU step i hVshift hη hη_compact hη_sub).grad x)) - ∫ (x : Vec d) in V, vecDot (G (euclideanCoordShift step i x)) ((localizedSqCutoffForwardDifferenceQuotientToAmbient u hV hVU step i hVshift hη hη_compact hη_sub).grad x))

The split direct-test gradient pairing reduces to two interior pairings: the unshifted pairing against G(x) and the transported shifted pairing against G(x+h e_i).

theorem HCPolySupport.WeakPoissonEquationOn.integral_dot_backwardDifference_cutoffGradient_eq_neg_integral_forwardDifference {d : ℕ} {U V : Set (Vec d)} {G : Vec d → Vec d} (hG : MemVectorL2 U G) (u : H1Function U) (hV : IsOpenBoundedConvexDomain V) (hVU : V ⊆ U) (step : ℝ) (i : Fin d) (hGshiftV : MemVectorL2 V fun (x : Vec d) => G (euclideanCoordShift step i x)) (hVshift : V ⊆ translateSet (-step • basisVec i) U) {η : Vec d → ℝ} (hη : ContDiff ℝ (↑⊤) η) (hη_compact : HasCompactSupport η) (hη_sub : tsupport η ⊆ V) : ∫ (x : Vec d) in U, vecDot (G x) ((backwardDifferenceQuotientSqCutoffForwardDifferenceQuotientToAmbient u hV hVU step i hVshift hη hη_compact hη_sub).grad x) = -∫ (x : Vec d) in V, vecDot (fun (j : Fin d) => euclideanForwardDifferenceQuotient step i (fun (y : Vec d) => G y j) x) ((localizedSqCutoffForwardDifferenceQuotientToAmbient u hV hVU step i hVshift hη hη_compact hη_sub).grad x)

The transported split is the negative of the interior pairing with the forward quotient of the vector field G.

theorem HCPolySupport.WeakPoissonEquationOn.memVectorL2_grad_comp_euclideanCoordShift_of_shift_subset {d : ℕ} {U V : Set (Vec d)} (u : H1Function U) (hV : IsOpenBoundedConvexDomain V) (step : ℝ) (i : Fin d) (hVshift : V ⊆ translateSet (-step • basisVec i) U) : MemVectorL2 V fun (x : Vec d) => u.grad (euclideanCoordShift step i x)

Shifted gradients remain L² on a shift-safe interior set.

theorem HCPolySupport.WeakPoissonEquationOn.forwardDifferenceQuotientOn_grad_eq_vectorForwardDifferenceQuotient {d : ℕ} {U V : Set (Vec d)} (u : H1Function U) (hV : IsOpenBoundedConvexDomain V) (hVU : V ⊆ U) (step : ℝ) (i : Fin d) (hVshift : V ⊆ translateSet (-step • basisVec i) U) (x : Vec d) : (u.forwardDifferenceQuotientOn step i ⋯ hVU hVshift).grad x = fun (j : Fin d) => euclideanForwardDifferenceQuotient step i (fun (y : Vec d) => u.grad y j) x

The gradient of the forward quotient is the coordinatewise forward quotient of the gradient.

theorem HCPolySupport.WeakPoissonEquationOn.integral_forwardDifferenceGradient_eq_neg_integral_forwardDifferenceDerivative {d : ℕ} {U V : Set (Vec d)} (u : H1Function U) (hV : IsOpenBoundedConvexDomain V) (hVU : V ⊆ U) {step : ℝ} (i j : Fin d) (hVshift : V ⊆ translateSet (-step • basisVec i) U) {φ : Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hφ_compact : HasCompactSupport φ) (hφ_sub : tsupport φ ⊆ V) : ∫ (x : Vec d) in V, (u.forwardDifferenceQuotientOn step i ⋯ hVU hVshift).grad x j * φ x = -∫ (x : Vec d) in V, euclideanForwardDifferenceQuotient step i u.toFun x * (fderiv ℝ φ x) (basisVec j)

Weak-gradient identity for one coordinate of a forward difference quotient.

This is the distributional handoff used by the Hessian limit argument: each coordinate of ∇D_i^+u pairs against a test as D_i^+u paired against the corresponding test derivative.

theorem HCPolySupport.WeakPoissonEquationOn.abs_integral_coordProduct_le_half_normSquares {d : ℕ} {U : Set (Vec d)} {G : Vec d → Vec d} {φ : Vec d → ℝ} (hG : MemVectorL2 U G) (hφ : MemScalarL2 U φ) (j : Fin d) : |∫ (x : Vec d) in U, G x j * φ x| ≤ (1 / 2 * ∫ (x : Vec d) in U, vecNormSq (G x)) + 1 / 2 * ∫ (x : Vec d) in U, φ x ^ 2

Coordinatewise L² pairing bound by the full vector energy and the scalar test energy.

theorem HCPolySupport.WeakPoissonEquationOn.abs_integral_coord_mul_le_half_integral_vectorNormSq_add_half_integral_sq {d : ℕ} {S V : Set (Vec d)} {G : Vec d → Vec d} {φ : Vec d → ℝ} (hSV : S ⊆ V) (hφ_support : Function.support φ ⊆ S) (hG : MemVectorL2 V G) (hφS : MemScalarL2 S φ) (j : Fin d) : |∫ (x : Vec d) in V, G x j * φ x| ≤ (1 / 2 * ∫ (x : Vec d) in S, vecNormSq (G x)) + 1 / 2 * ∫ (x : Vec d) in S, φ x ^ 2

Version of the coordinatewise L² pairing bound localized by support: when the scalar test is supported in S ⊆ V, only the energy on S appears.

theorem HCPolySupport.WeakPoissonEquationOn.abs_integral_coord_mul_le_l2_mul_l2_of_memVectorL2_memScalarL2 {d : ℕ} {U : Set (Vec d)} {G : Vec d → Vec d} {φ : Vec d → ℝ} (hG : MemVectorL2 U G) (hφ : MemScalarL2 U φ) (j : Fin d) : |∫ (x : Vec d) in U, G x j * φ x| ≤ (∫ (x : Vec d) in U, ‖G x j‖ ^ 2) ^ (1 / 2) * (∫ (x : Vec d) in U, ‖φ x‖ ^ 2) ^ (1 / 2)

Coordinatewise Cauchy-Schwarz pairing bound in L². Unlike the Young form above, this is homogeneous in the test norm and is the shape needed for a Riesz/weak-limit handoff.

theorem HCPolySupport.WeakPoissonEquationOn.abs_integral_coord_mul_le_l2_mul_l2_subset_of_support_subset {d : ℕ} {S V : Set (Vec d)} {G : Vec d → Vec d} {φ : Vec d → ℝ} (hSV : S ⊆ V) (hφ_support : Function.support φ ⊆ S) (hG : MemVectorL2 V G) (hφS : MemScalarL2 S φ) (j : Fin d) : |∫ (x : Vec d) in V, G x j * φ x| ≤ (∫ (x : Vec d) in S, ‖G x j‖ ^ 2) ^ (1 / 2) * (∫ (x : Vec d) in S, ‖φ x‖ ^ 2) ^ (1 / 2)

Support-localized Cauchy-Schwarz pairing bound.

theorem HCPolySupport.WeakPoissonEquationOn.integral_coord_norm_rpow_two_le_integral_vecNormSq_of_memVectorL2 {d : ℕ} {U : Set (Vec d)} {G : Vec d → Vec d} (hG : MemVectorL2 U G) (j : Fin d) : ∫ (x : Vec d) in U, ‖G x j‖ ^ 2 ≤ ∫ (x : Vec d) in U, vecNormSq (G x)

The L² energy of one coordinate is bounded by the full vector-field energy.

theorem HCPolySupport.WeakPoissonEquationOn.abs_neg_integral_forwardDifferenceQuotient_mul_fderiv_le_l2_mul_l2_on_inner {d : ℕ} {U V : Set (Vec d)} (u : H1Function U) (hV : IsOpenBoundedConvexDomain V) (hVU : V ⊆ U) {step : ℝ} (i j : Fin d) (hVshift : V ⊆ translateSet (-step • basisVec i) U) {S : Set (Vec d)} (hSV : S ⊆ V) {φ : Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hφ_compact : HasCompactSupport φ) (hφ_subS : tsupport φ ⊆ S) : |(-∫ (x : Vec d) in V, euclideanForwardDifferenceQuotient step i u.toFun x * (fderiv ℝ φ x) (basisVec j))| ≤ (∫ (x : Vec d) in S, ‖(u.forwardDifferenceQuotientOn step i ⋯ hVU hVshift).grad x j‖ ^ 2) ^ (1 / 2) * (∫ (x : Vec d) in S, ‖φ x‖ ^ 2) ^ (1 / 2)

Homogeneous weak-Hessian handoff from the quotient-gradient coordinate to the distributional second-derivative test functional.

theorem HCPolySupport.WeakPoissonEquationOn.abs_neg_integral_forwardDifferenceQuotient_mul_fderiv_le_grad_l2_mul_l2_on_inner {d : ℕ} {U V : Set (Vec d)} (u : H1Function U) (hV : IsOpenBoundedConvexDomain V) (hVU : V ⊆ U) {step : ℝ} (i j : Fin d) (hVshift : V ⊆ translateSet (-step • basisVec i) U) {S : Set (Vec d)} (hSV : S ⊆ V) {φ : Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hφ_compact : HasCompactSupport φ) (hφ_subS : tsupport φ ⊆ S) : |(-∫ (x : Vec d) in V, euclideanForwardDifferenceQuotient step i u.toFun x * (fderiv ℝ φ x) (basisVec j))| ≤ (∫ (x : Vec d) in S, vecNormSq ((u.forwardDifferenceQuotientOn step i ⋯ hVU hVshift).grad x)) ^ (1 / 2) * (∫ (x : Vec d) in S, ‖φ x‖ ^ 2) ^ (1 / 2)

Homogeneous weak-Hessian handoff controlled by the full quotient-gradient energy on the inner set.

theorem HCPolySupport.WeakPoissonEquationOn.abs_neg_integral_forwardDifferenceQuotient_mul_fderiv_le_sqrt_energy_bound_mul_l2 {d : ℕ} {U V : Set (Vec d)} (u : H1Function U) (hV : IsOpenBoundedConvexDomain V) (hVU : V ⊆ U) {step R : ℝ} (i j : Fin d) (hVshift : V ⊆ translateSet (-step • basisVec i) U) {S : Set (Vec d)} (hSV : S ⊆ V) {φ : Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hφ_compact : HasCompactSupport φ) (hφ_subS : tsupport φ ⊆ S) (henergy : 1 / 4 * ∫ (x : Vec d) in S, vecNormSq ((u.forwardDifferenceQuotientOn step i ⋯ hVU hVshift).grad x) ≤ R) : |(-∫ (x : Vec d) in V, euclideanForwardDifferenceQuotient step i u.toFun x * (fderiv ℝ φ x) (basisVec j))| ≤ (4 * R) ^ (1 / 2) * (∫ (x : Vec d) in S, ‖φ x‖ ^ 2) ^ (1 / 2)

Homogeneous weak-Hessian handoff from an inner full-gradient energy bound.

theorem HCPolySupport.WeakPoissonEquationOn.neg_integral_forwardDifferenceQuotient_mul_fderiv_eq_zero_of_l2_norm_zero_on_inner {d : ℕ} {U V : Set (Vec d)} (u : H1Function U) (hV : IsOpenBoundedConvexDomain V) (hVU : V ⊆ U) {step R : ℝ} (i j : Fin d) (hVshift : V ⊆ translateSet (-step • basisVec i) U) {S : Set (Vec d)} (hSV : S ⊆ V) {φ : Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hφ_compact : HasCompactSupport φ) (hφ_subS : tsupport φ ⊆ S) (henergy : 1 / 4 * ∫ (x : Vec d) in S, vecNormSq ((u.forwardDifferenceQuotientOn step i ⋯ hVU hVshift).grad x) ≤ R) (hφ_zero : ∫ (x : Vec d) in S, ‖φ x‖ ^ 2 = 0) : -∫ (x : Vec d) in V, euclideanForwardDifferenceQuotient step i u.toFun x * (fderiv ℝ φ x) (basisVec j) = 0

If the inner L² seminorm of the smooth test is zero, then the distributional quotient-Hessian pairing vanishes. This is the elementary well-definedness plank needed before extending the bounded test functional to the L² quotient space.

theorem HCPolySupport.WeakPoissonEquationOn.neg_integral_forwardDifferenceQuotient_mul_fderiv_eq_of_l2_dist_zero_on_inner {d : ℕ} {U V : Set (Vec d)} (u : H1Function U) (hV : IsOpenBoundedConvexDomain V) (hVU : V ⊆ U) {step R : ℝ} (i j : Fin d) (hVshift : V ⊆ translateSet (-step • basisVec i) U) {S : Set (Vec d)} (hSV : S ⊆ V) {φ ψ : Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hψ : ContDiff ℝ (↑⊤) ψ) (hφ_compact : HasCompactSupport φ) (hψ_compact : HasCompactSupport ψ) (hφ_subS : tsupport φ ⊆ S) (hψ_subS : tsupport ψ ⊆ S) (henergy : 1 / 4 * ∫ (x : Vec d) in S, vecNormSq ((u.forwardDifferenceQuotientOn step i ⋯ hVU hVshift).grad x) ≤ R) (hφψ_zero : ∫ (x : Vec d) in S, ‖φ x - ψ x‖ ^ 2 = 0) : -∫ (x : Vec d) in V, euclideanForwardDifferenceQuotient step i u.toFun x * (fderiv ℝ φ x) (basisVec j) = -∫ (x : Vec d) in V, euclideanForwardDifferenceQuotient step i u.toFun x * (fderiv ℝ ψ x) (basisVec j)

If two smooth compact tests have zero L² distance on the inner support set, then they give the same distributional quotient-Hessian pairing. The proof rewrites the derivative-side pairing through the weak-gradient identity, so the linearity step happens on the value side as ordinary L² algebra.