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

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

theorem HCPolySupport.WeakPoissonEquationOn.openCubeInnerOpenCubeQuotientHessianPairing_eq_integral_mul_backwardDifferenceQuotient_deriv {d : ℕ} {V : Set (Vec d)} {Q : TriadicCube d} (uQ : H1Function (openCubeSet Q)) {step : ℝ} (i j : Fin d) {ρ₁ : ℝ} (φ : H1WeakTestFunction (scaledOpenCubeSet Q ρ₁)) (hSV : scaledOpenCubeSet Q ρ₁ ⊆ V) (hshiftInt : MeasureTheory.Integrable (fun (x : Vec d) => uQ.toFun (euclideanCoordShift step i x) * φ.deriv j x) MeasureTheory.volume) (huvInt : MeasureTheory.Integrable (fun (x : Vec d) => uQ.toFun x * φ.deriv j x) MeasureTheory.volume) (hbackShiftInt : MeasureTheory.Integrable (fun (x : Vec d) => uQ.toFun x * φ.deriv j (euclideanCoordShift (-step) i x)) MeasureTheory.volume) : openCubeInnerOpenCubeQuotientHessianPairing uQ V step i j φ = ∫ (x : Vec d), uQ.toFun x * euclideanBackwardDifferenceQuotient step i (fun (y : Vec d) => φ.deriv j y) x

Fixed-step open-inner Hessian pairings can be moved from the forward quotient on the rough potential to the backward quotient on the smooth test derivative.

This is the concrete bridge from the quotient estimate to the limiting weak second derivative: the nonsmooth H¹ representative appears only as an L¹-paired factor.

theorem HCPolySupport.WeakPoissonEquationOn.innerCubeHessianPairing_eq_integral_mul_backwardDifference_deriv {d : ℕ} {V : Set (Vec d)} {Q : TriadicCube d} (uQ : H1Function (openCubeSet Q)) {step : ℝ} (i j : Fin d) {ρ₁ : ℝ} (φ : H1WeakTestFunction (scaledOpenCubeSet Q ρ₁)) (hSV : scaledOpenCubeSet Q ρ₁ ⊆ V) (hVU : V ⊆ openCubeSet Q) (hVshift : ∀ x ∈ V, euclideanCoordShift step i x ∈ openCubeSet Q) : openCubeInnerOpenCubeQuotientHessianPairing uQ V step i j φ = ∫ (x : Vec d), uQ.toFun x * euclideanBackwardDifferenceQuotient step i (fun (y : Vec d) => φ.deriv j y) x

Fixed-step pairing rewrite with the L1 hypotheses discharged from the interior support and one-step cube-margin conditions.

theorem HCPolySupport.WeakPoissonEquationOn.integral_mul_fderiv_h1WeakTest_deriv_eq_openCubeInnerOpenCubeLimitHessianPairing {d : ℕ} {V : Set (Vec d)} {Q : TriadicCube d} (uQ : H1Function (openCubeSet Q)) (i j : Fin d) {ρ₁ : ℝ} (φ : H1WeakTestFunction (scaledOpenCubeSet Q ρ₁)) (hSV : scaledOpenCubeSet Q ρ₁ ⊆ V) (hVU : V ⊆ openCubeSet Q) : ∫ (x : Vec d), uQ.toFun x * (fderiv ℝ (fun (y : Vec d) => φ.deriv j y) x) (basisVec i) = openCubeInnerOpenCubeLimitHessianPairing uQ V i j φ

The classical limit of the smooth-test summation-by-parts expression is the desired limiting Hessian pairing.

theorem HCPolySupport.WeakPoissonEquationOn.openCubeInnerHessianPairingTendsto_of_integral_backwardDifferenceQuotient_deriv_tendsto {d : ℕ} {V : Set (Vec d)} {Q : TriadicCube d} (uQ : H1Function (openCubeSet Q)) (stepSeq : ℕ → ℝ) (i j : Fin d) {ρ₁ : ℝ} (hSV : scaledOpenCubeSet Q ρ₁ ⊆ V) (hVU : V ⊆ openCubeSet Q) (hVshift : ∀ (n : ℕ), ∀ x ∈ V, euclideanCoordShift (stepSeq n) i x ∈ openCubeSet Q) (hback_lim : ∀ (φ : H1WeakTestFunction (scaledOpenCubeSet Q ρ₁)), Filter.Tendsto (fun (n : ℕ) => ∫ (x : Vec d), uQ.toFun x * euclideanBackwardDifferenceQuotient (stepSeq n) i (fun (y : Vec d) => φ.deriv j y) x) Filter.atTop (nhds (∫ (x : Vec d), uQ.toFun x * (fderiv ℝ (fun (y : Vec d) => φ.deriv j y) x) (basisVec i)))) : OpenCubeInnerHessianPairingTendsto uQ V stepSeq i j

The remaining smooth-test convergence statement implies the OpenCubeInnerHessianPairingTendsto interface consumed by the limiting Riesz construction.