Coarse-graining support: Support.Sobolev.Foundations.CubeNeumannW22CZ.WeakInteriorDQ.SqCutoffH10

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

theorem HCPolySupport.WeakPoissonEquationOn.memH10_sqCutoffForwardDifferenceQuotient {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) {η : Vec d → ℝ} (hη : ContDiff ℝ (↑⊤) η) (hη_compact : HasCompactSupport η) (hη_sub : tsupport η ⊆ V) : MemH10 U fun (x : Vec d) => η x ^ 2 * euclideanForwardDifferenceQuotient step i u.toFun x

The squared-cutoff forward difference quotient η² D_i^+ u is an ambient zero-trace test when the cutoff is supported in a shift-safe interior set.

theorem HCPolySupport.WeakPoissonEquationOn.support_sqCutoffForwardDifferenceQuotient_subset {d : ℕ} {U V : Set (Vec d)} (u : H1Function U) (hVU : V ⊆ U) (step : ℝ) (i : Fin d) {η : Vec d → ℝ} (hη_sub : tsupport η ⊆ V) : (Function.support fun (x : Vec d) => η x ^ 2 * euclideanForwardDifferenceQuotient step i u.toFun x) ⊆ U

The squared-cutoff forward quotient is genuinely supported in the ambient domain when the cutoff support lies in an interior subset.

noncomputable def HCPolySupport.WeakPoissonEquationOn.sqCutoffForwardDifferenceQuotientToH10 {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) {η : Vec d → ℝ} (hη : ContDiff ℝ (↑⊤) η) (hη_compact : HasCompactSupport η) (hη_sub : tsupport η ⊆ V) : H10Function U

Chosen ambient H¹₀(U) representative of η² D_i^+ u.

Equations

• HCPolySupport.WeakPoissonEquationOn.sqCutoffForwardDifferenceQuotientToH10 u hV hVU step i hVshift hη hη_compact hη_sub = Classical.choose ⋯

@[simp]

theorem HCPolySupport.WeakPoissonEquationOn.sqCutoffForwardDifferenceQuotientToH10_toFun {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) {η : Vec d → ℝ} (hη : ContDiff ℝ (↑⊤) η) (hη_compact : HasCompactSupport η) (hη_sub : tsupport η ⊆ V) : (sqCutoffForwardDifferenceQuotientToH10 u hV hVU step i hVshift hη hη_compact hη_sub).toFun = fun (x : Vec d) => η x ^ 2 * euclideanForwardDifferenceQuotient step i u.toFun x

theorem HCPolySupport.WeakPoissonEquationOn.sqCutoffForwardDifferenceQuotientToH10_grad_coord_ae {d : ℕ} {U V : Set (Vec d)} (hU : IsOpen U) (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) : (fun (x : Vec d) => (sqCutoffForwardDifferenceQuotientToH10 u hV hVU step i hVshift hη hη_compact hη_sub).grad x j) =ᵐ[MeasureTheory.volume.restrict U] fun (x : Vec d) => (localizedSqCutoffForwardDifferenceQuotientToAmbient u hV hVU step i hVshift hη hη_compact hη_sub).grad x j

Coordinatewise gradient identification between the chosen ambient H¹₀(U) representative of η²D_i^+u and the explicit ambient H¹ localized product representative.

theorem HCPolySupport.WeakPoissonEquationOn.sqCutoffForwardDifferenceQuotientToH10_grad_ae {d : ℕ} {U V : Set (Vec d)} (hU : IsOpen U) (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) : (fun (x : Vec d) => (sqCutoffForwardDifferenceQuotientToH10 u hV hVU step i hVshift hη hη_compact hη_sub).grad x) =ᵐ[MeasureTheory.volume.restrict U] fun (x : Vec d) => (localizedSqCutoffForwardDifferenceQuotientToAmbient u hV hVU step i hVshift hη hη_compact hη_sub).grad x

Vector-valued gradient identification for the chosen ambient H¹₀(U) representative of η²D_i^+u.

theorem HCPolySupport.WeakPoissonEquationOn.eLpNorm_backwardDifference_cutoffForwardDifference_le_eLpNorm_H10Gradient {d : ℕ} {U V : Set (Vec d)} (hU : IsOpen U) (u : H1Function U) (hV : IsOpenBoundedConvexDomain V) (hVU : V ⊆ U) {step : ℝ} (hstep : step ≠ 0) (i : Fin d) (hVshift : V ⊆ translateSet (-step • basisVec i) U) {η : Vec d → ℝ} (hη : ContDiff ℝ (↑⊤) η) (hη_compact : HasCompactSupport η) (hη_sub : tsupport η ⊆ V) : MeasureTheory.eLpNorm (euclideanBackwardDifferenceQuotient step i fun (y : Vec d) => η y ^ 2 * euclideanForwardDifferenceQuotient step i u.toFun y) 2 MeasureTheory.volume ≤ MeasureTheory.eLpNorm (fun (x : Vec d) => (sqCutoffForwardDifferenceQuotientToH10 u hV hVU step i hVshift hη hη_compact hη_sub).grad x i) 2 (MeasureTheory.volume.restrict U)

The whole-space backward quotient bound specialized to the squared-cutoff forward difference quotient test.

theorem HCPolySupport.WeakPoissonEquationOn.eLpNorm_backwardDifference_cutoffForwardDifference_le_eLpNorm_cutoffGradient {d : ℕ} {U V : Set (Vec d)} (hU : IsOpen U) (u : H1Function U) (hV : IsOpenBoundedConvexDomain V) (hVU : V ⊆ U) {step : ℝ} (hstep : step ≠ 0) (i : Fin d) (hVshift : V ⊆ translateSet (-step • basisVec i) U) {η : Vec d → ℝ} (hη : ContDiff ℝ (↑⊤) η) (hη_compact : HasCompactSupport η) (hη_sub : tsupport η ⊆ V) : MeasureTheory.eLpNorm (euclideanBackwardDifferenceQuotient step i fun (y : Vec d) => η y ^ 2 * euclideanForwardDifferenceQuotient step i u.toFun y) 2 MeasureTheory.volume ≤ MeasureTheory.eLpNorm (fun (x : Vec d) => (localizedSqCutoffForwardDifferenceQuotientToAmbient u hV hVU step i hVshift hη hη_compact hη_sub).grad x i) 2 (MeasureTheory.volume.restrict U)

The squared-cutoff direct test is controlled by the explicit product-rule gradient of η²D_i^+u.

theorem HCPolySupport.WeakPoissonEquationOn.memH10_sqShiftedCutoffBackwardDifferenceQuotient {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) {η : Vec d → ℝ} (hη : ContDiff ℝ (↑⊤) η) (hη_compact : HasCompactSupport η) (hη_sub : tsupport η ⊆ V) : MemH10 U fun (x : Vec d) => η (euclideanCoordShift (-step) i x) ^ 2 * euclideanBackwardDifferenceQuotient step i u.toFun x

The shifted factor η(x-h e_i)² D_i^- u(x) is an ambient zero-trace test. It is the translated companion to memH10_sqCutoffForwardDifferenceQuotient, with the backward quotient living on the translated interior set V + h e_i.

noncomputable def HCPolySupport.WeakPoissonEquationOn.localizedSqShiftedCutoffBackwardDifferenceQuotientToAmbient {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) {η : Vec d → ℝ} (hη : ContDiff ℝ (↑⊤) η) (hη_compact : HasCompactSupport η) (hη_sub : tsupport η ⊆ V) : H1Function U

Ambient H¹ representative of the shifted term η(x-h e_i)² D_i^- u(x), localized on the translated interior set V + h e_i.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem HCPolySupport.WeakPoissonEquationOn.localizedSqShiftedCutoffBackwardDifferenceQuotientToAmbient_toFun {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) {η : Vec d → ℝ} (hη : ContDiff ℝ (↑⊤) η) (hη_compact : HasCompactSupport η) (hη_sub : tsupport η ⊆ V) : (localizedSqShiftedCutoffBackwardDifferenceQuotientToAmbient u hV hVU step i hVshift hη hη_compact hη_sub).toFun = fun (x : Vec d) => η (euclideanCoordShift (-step) i x) ^ 2 * euclideanBackwardDifferenceQuotient step i u.toFun x

theorem HCPolySupport.WeakPoissonEquationOn.localizedSqShiftedCutoffBackwardDifferenceQuotientToAmbient_grad_eq_shift {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) {η : Vec d → ℝ} (hη : ContDiff ℝ (↑⊤) η) (hη_compact : HasCompactSupport η) (hη_sub : tsupport η ⊆ V) (x : Vec d) : (localizedSqShiftedCutoffBackwardDifferenceQuotientToAmbient u hV hVU step i hVshift hη hη_compact hη_sub).grad x = (localizedSqCutoffForwardDifferenceQuotientToAmbient u hV hVU step i hVshift hη hη_compact hη_sub).grad (euclideanCoordShift (-step) i x)

theorem HCPolySupport.WeakPoissonEquationOn.support_vecDot_localizedSqShiftedCutoffBackwardDifferenceQuotientToAmbient_grad_subset {d : ℕ} {U V : Set (Vec d)} (G : Vec d → Vec d) (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) : (Function.support fun (x : Vec d) => vecDot (G x) ((localizedSqShiftedCutoffBackwardDifferenceQuotientToAmbient u hV hVU step i hVshift hη hη_compact hη_sub).grad x)) ⊆ translateSet (step • basisVec i) V

Pairing against the shifted localized gradient is supported in the translated interior set.

theorem HCPolySupport.WeakPoissonEquationOn.shiftedCutoff_backwardGradient_integral_eq_forward {d : ℕ} {U V : Set (Vec d)} (G : Vec d → Vec d) (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) ((localizedSqShiftedCutoffBackwardDifferenceQuotientToAmbient 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)

Transport the shifted localized-gradient pairing from U back to the interior set V.

noncomputable def HCPolySupport.WeakPoissonEquationOn.backwardDifferenceQuotientSqCutoffForwardDifferenceQuotientToAmbient {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) {η : Vec d → ℝ} (hη : ContDiff ℝ (↑⊤) η) (hη_compact : HasCompactSupport η) (hη_sub : tsupport η ⊆ V) : H1Function U

Explicit ambient H¹ representative of the direct test D_i^-(η² D_i^+u).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem HCPolySupport.WeakPoissonEquationOn.backwardDifferenceQuotientSqCutoffForwardDifferenceQuotientToAmbient_toFun {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) {η : Vec d → ℝ} (hη : ContDiff ℝ (↑⊤) η) (hη_compact : HasCompactSupport η) (hη_sub : tsupport η ⊆ V) : (backwardDifferenceQuotientSqCutoffForwardDifferenceQuotientToAmbient u hV hVU step i hVshift hη hη_compact hη_sub).toFun = euclideanBackwardDifferenceQuotient step i fun (x : Vec d) => η x ^ 2 * euclideanForwardDifferenceQuotient step i u.toFun x

theorem HCPolySupport.WeakPoissonEquationOn.support_backwardDifferenceQuotient_sqCutoffForwardDifferenceQuotient_subset {d : ℕ} {U V : Set (Vec d)} (u : H1Function U) (hVU : V ⊆ U) (step : ℝ) (i : Fin d) (hVshift : V ⊆ translateSet (-step • basisVec i) U) {η : Vec d → ℝ} (hη_sub : tsupport η ⊆ V) : Function.support (euclideanBackwardDifferenceQuotient step i fun (x : Vec d) => η x ^ 2 * euclideanForwardDifferenceQuotient step i u.toFun x) ⊆ U

The direct difference-quotient test D_i^-(η²D_i^+u) is genuinely supported in the ambient domain.

@[simp]

theorem HCPolySupport.WeakPoissonEquationOn.backwardDifferenceQuotientSqCutoffForwardDifferenceQuotientToAmbient_grad {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) {η : Vec d → ℝ} (hη : ContDiff ℝ (↑⊤) η) (hη_compact : HasCompactSupport η) (hη_sub : tsupport η ⊆ V) : (backwardDifferenceQuotientSqCutoffForwardDifferenceQuotientToAmbient u hV hVU step i hVshift hη hη_compact hη_sub).grad = fun (x : Vec d) => 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)

theorem HCPolySupport.WeakPoissonEquationOn.memH10_backwardDifferenceQuotient_sqCutoffForwardDifferenceQuotient {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) {η : Vec d → ℝ} (hη : ContDiff ℝ (↑⊤) η) (hη_compact : HasCompactSupport η) (hη_sub : tsupport η ⊆ V) : MemH10 U (euclideanBackwardDifferenceQuotient step i fun (x : Vec d) => η x ^ 2 * euclideanForwardDifferenceQuotient step i u.toFun x)

The direct weak-equation test D_i^- (η² D_i^+ u) is ambient zero-trace.

This is the key admissibility bridge for the direct difference-quotient energy estimate: the original weak equation can be tested against a difference quotient of the cutoff-weighted forward quotient, so the forcing remains f rather than D_i^+ f.

noncomputable def HCPolySupport.WeakPoissonEquationOn.backwardDifferenceQuotientSqCutoffForwardDifferenceQuotientToH10 {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) {η : Vec d → ℝ} (hη : ContDiff ℝ (↑⊤) η) (hη_compact : HasCompactSupport η) (hη_sub : tsupport η ⊆ V) : H10Function U

Chosen H¹₀(U) representative of the direct difference-quotient test D_i^- (η² D_i^+ u).

Equations

• HCPolySupport.WeakPoissonEquationOn.backwardDifferenceQuotientSqCutoffForwardDifferenceQuotientToH10 u hV hVU step i hVshift hη hη_compact hη_sub = Classical.choose ⋯

@[simp]

theorem HCPolySupport.WeakPoissonEquationOn.backwardDifferenceQuotientSqCutoffForwardDifferenceQuotientToH10_toFun {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) {η : Vec d → ℝ} (hη : ContDiff ℝ (↑⊤) η) (hη_compact : HasCompactSupport η) (hη_sub : tsupport η ⊆ V) : (backwardDifferenceQuotientSqCutoffForwardDifferenceQuotientToH10 u hV hVU step i hVshift hη hη_compact hη_sub).toFun = euclideanBackwardDifferenceQuotient step i fun (x : Vec d) => η x ^ 2 * euclideanForwardDifferenceQuotient step i u.toFun x

theorem HCPolySupport.WeakPoissonEquationOn.backwardDifferenceQuotientSqCutoffForwardDifferenceQuotientToH10_grad_coord_ae {d : ℕ} {U V : Set (Vec d)} (hU : IsOpen U) (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) : (fun (x : Vec d) => (backwardDifferenceQuotientSqCutoffForwardDifferenceQuotientToH10 u hV hVU step i hVshift hη hη_compact hη_sub).grad x j) =ᵐ[MeasureTheory.volume.restrict U] fun (x : Vec d) => (backwardDifferenceQuotientSqCutoffForwardDifferenceQuotientToAmbient u hV hVU step i hVshift hη hη_compact hη_sub).grad x j

Coordinatewise gradient identification between the chosen H¹₀ representative of D_i^-(η² D_i^+u) and the explicit ambient H¹ representative built from localized shifted pieces.

theorem HCPolySupport.WeakPoissonEquationOn.backwardDifferenceQuotientSqCutoffForwardDifferenceQuotientToH10_grad_ae {d : ℕ} {U V : Set (Vec d)} (hU : IsOpen U) (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) : (fun (x : Vec d) => (backwardDifferenceQuotientSqCutoffForwardDifferenceQuotientToH10 u hV hVU step i hVshift hη hη_compact hη_sub).grad x) =ᵐ[MeasureTheory.volume.restrict U] fun (x : Vec d) => (backwardDifferenceQuotientSqCutoffForwardDifferenceQuotientToAmbient u hV hVU step i hVshift hη hη_compact hη_sub).grad x

Vector-valued gradient identification for the direct difference-quotient test.

theorem HCPolySupport.WeakPoissonEquationOn.integral_backwardDifference_cutoffForwardDifference_le_integral_cutoffGradient {d : ℕ} {U V : Set (Vec d)} (hU : IsOpen U) (u : H1Function U) (hV : IsOpenBoundedConvexDomain V) (hVU : V ⊆ U) {step : ℝ} (hstep : step ≠ 0) (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, euclideanBackwardDifferenceQuotient step i (fun (y : Vec d) => η y ^ 2 * euclideanForwardDifferenceQuotient step i u.toFun y) x ^ 2 ≤ ∫ (x : Vec d) in U, (localizedSqCutoffForwardDifferenceQuotientToAmbient u hV hVU step i hVshift hη hη_compact hη_sub).grad x i ^ 2

Integral-square form of the specialized direct-test quotient bound.

theorem HCPolySupport.WeakPoissonEquationOn.test_backwardDifferenceQuotient_sqCutoffForwardDifferenceQuotientToH10 {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) ((backwardDifferenceQuotientSqCutoffForwardDifferenceQuotientToH10 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

Original weak equation tested against the direct difference-quotient test. The right-hand side contains the undifferentiated forcing f; the next stage is to identify the left-hand side by finite-difference summation by parts.

theorem HCPolySupport.WeakPoissonEquationOn.test_backwardDifferenceQuotient_sqCutoffForwardDifferenceQuotient_explicitGradient {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) ((backwardDifferenceQuotientSqCutoffForwardDifferenceQuotientToAmbient 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

Original weak equation tested against the direct difference-quotient test, with the left-hand side rewritten using the explicit ambient H¹ representative of that test.