Coarse-graining support:

Support.Sobolev.Foundations.CubeNeumannW22CZ.WeakInteriorDQ.DiffQuotientLp

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

theorem HCPolySupport.WeakPoissonEquationOn.tendsto_eLpNorm_h10_approx_sub_toFun_global_of_support_subset {d : ℕ} {U : Set (Vec d)} (ψ : H10Function U) (hψ_support : Function.support ψ.toFun ⊆ U) : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (x : Vec d) => ψ.approx n x - ψ.toFun x) 2 MeasureTheory.volume) Filter.atTop (nhds 0)

The H¹₀ scalar approximants converge globally whenever both the limit and the approximants are genuinely supported in the domain.

theorem HCPolySupport.WeakPoissonEquationOn.aestronglyMeasurable_h10_approx_sub_toFun_global_of_support_subset {d : ℕ} {U : Set (Vec d)} (hU_meas : MeasurableSet U) (ψ : H10Function U) (hψ_support : Function.support ψ.toFun ⊆ U) (n : ℕ) : MeasureTheory.AEStronglyMeasurable (fun (x : Vec d) => ψ.approx n x - ψ.toFun x) MeasureTheory.volume

The scalar H¹₀ approximation errors are globally a.e.-strongly-measurable when their support is genuinely contained in the domain.

theorem HCPolySupport.WeakPoissonEquationOn.tendsto_eLpNorm_h10_backwardDifferenceQuotient_approx_sub_toFun_global {d : ℕ} {U : Set (Vec d)} (hU_meas : MeasurableSet U) (ψ : H10Function U) (hψ_support : Function.support ψ.toFun ⊆ U) (step : ℝ) (i : Fin d) : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (x : Vec d) => euclideanBackwardDifferenceQuotient step i (ψ.approx n) x - euclideanBackwardDifferenceQuotient step i ψ.toFun x) 2 MeasureTheory.volume) Filter.atTop (nhds 0)

Global convergence of the backward difference quotients of the H¹₀ approximants to the backward difference quotient of the H¹₀ limit.

theorem HCPolySupport.WeakPoissonEquationOn.eLpNorm_h10_backwardDifferenceQuotient_le_eLpNorm_grad {d : ℕ} {U : Set (Vec d)} (hU_meas : MeasurableSet U) (ψ : H10Function U) (hψ_support : Function.support ψ.toFun ⊆ U) {step : ℝ} (hstep : step ≠ 0) (i : Fin d) : MeasureTheory.eLpNorm (euclideanBackwardDifferenceQuotient step i ψ.toFun) 2 MeasureTheory.volume ≤ MeasureTheory.eLpNorm (fun (x : Vec d) => ψ.grad x i) 2 (MeasureTheory.volume.restrict U)

The smooth whole-space quotient estimate passes to a genuinely supported H¹₀(U) limit. This is the zero-trace version of eLpNorm_euclideanBackwardDifferenceQuotient_le_eLpNorm_coordDeriv: the derivative side is the weak gradient coordinate on U.

theorem HCPolySupport.WeakPoissonEquationOn.memLp_h10_backwardDifferenceQuotient_of_support_subset {d : ℕ} {U : Set (Vec d)} (hU_meas : MeasurableSet U) (ψ : H10Function U) (hψ_support : Function.support ψ.toFun ⊆ U) {step : ℝ} (hstep : step ≠ 0) (i : Fin d) : MeasureTheory.MemLp (euclideanBackwardDifferenceQuotient step i ψ.toFun) 2 MeasureTheory.volume

The global backward quotient of a genuinely supported H¹₀(U) function is an L²(ℝᵈ) function.

theorem HCPolySupport.WeakPoissonEquationOn.eLpNorm_h10_forwardDifferenceQuotient_le_eLpNorm_grad {d : ℕ} {U : Set (Vec d)} (hU_meas : MeasurableSet U) (ψ : H10Function U) (hψ_support : Function.support ψ.toFun ⊆ U) {step : ℝ} (hstep : step ≠ 0) (i : Fin d) : MeasureTheory.eLpNorm (euclideanForwardDifferenceQuotient step i ψ.toFun) 2 MeasureTheory.volume ≤ MeasureTheory.eLpNorm (fun (x : Vec d) => ψ.grad x i) 2 (MeasureTheory.volume.restrict U)

Forward version of the H¹₀ quotient estimate.

theorem HCPolySupport.WeakPoissonEquationOn.memLp_h10_forwardDifferenceQuotient_of_support_subset {d : ℕ} {U : Set (Vec d)} (hU_meas : MeasurableSet U) (ψ : H10Function U) (hψ_support : Function.support ψ.toFun ⊆ U) {step : ℝ} (hstep : step ≠ 0) (i : Fin d) : MeasureTheory.MemLp (euclideanForwardDifferenceQuotient step i ψ.toFun) 2 MeasureTheory.volume

The global forward quotient of a genuinely supported H¹₀(U) function is an L²(ℝᵈ) function.

theorem HCPolySupport.WeakPoissonEquationOn.integral_forwardDifferenceQuotient_sq_le_integral_h10_grad_sq {d : ℕ} {U : Set (Vec d)} (hU_meas : MeasurableSet U) (ψ : H10Function U) (hψ_support : Function.support ψ.toFun ⊆ U) {step : ℝ} (hstep : step ≠ 0) (i : Fin d) : ∫ (x : Vec d), euclideanForwardDifferenceQuotient step i ψ.toFun x ^ 2 ≤ ∫ (x : Vec d) in U, ψ.grad x i ^ 2

Integral-square form of the forward H¹₀ quotient estimate.

theorem HCPolySupport.WeakPoissonEquationOn.integral_set_forwardDifferenceQuotient_sq_le_integral_h10_grad_sq {d : ℕ} {U : Set (Vec d)} (hU_meas : MeasurableSet U) (ψ : H10Function U) (hψ_support : Function.support ψ.toFun ⊆ U) (S : Set (Vec d)) {step : ℝ} (hstep : step ≠ 0) (i : Fin d) : ∫ (x : Vec d) in S, euclideanForwardDifferenceQuotient step i ψ.toFun x ^ 2 ≤ ∫ (x : Vec d) in U, ψ.grad x i ^ 2

Set-localized integral-square form of the forward H¹₀ quotient estimate.

theorem HCPolySupport.WeakPoissonEquationOn.integral_set_forwardDifferenceQuotient_sq_le_integral_localized_h10_grad_sq {d : ℕ} {U : Set (Vec d)} (u : H1Function U) (hU : IsOpenBoundedConvexDomain U) {φ : Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hφ_compact : HasCompactSupport φ) (hφ_sub : tsupport φ ⊆ U) {S : Set (Vec d)} (hS_meas : MeasurableSet S) {step : ℝ} (hstep : step ≠ 0) (i : Fin d) (hφ_one : ∀ x ∈ S, φ x = 1) (hφ_shift_one : ∀ x ∈ S, φ (euclideanCoordShift step i x) = 1) : ∫ (x : Vec d) in S, euclideanForwardDifferenceQuotient step i u.toFun x ^ 2 ≤ ∫ (x : Vec d) in U, (u.mulContDiffHasCompactSupportToH10 hU hφ hφ_compact hφ_sub).grad x i ^ 2

Lower-order quotient control for a function localized by a cutoff which is one on the set of integration and on its forward coordinate shift.

theorem HCPolySupport.WeakPoissonEquationOn.memScalarL2_mul_of_contDiff_hasCompactSupport_tsupport_subset {d : ℕ} {U V : Set (Vec d)} {φ F : Vec d → ℝ} (hV_meas : MeasurableSet V) (hφ : ContDiff ℝ (↑⊤) φ) (hφ_compact : HasCompactSupport φ) (hφ_sub : tsupport φ ⊆ V) (hF : MemScalarL2 V F) : MemScalarL2 U fun (x : Vec d) => φ x * F x

A smooth compactly supported cutoff localizes a scalar L²(V) function to an ambient scalar L²(U) function when the cutoff support lies in V.