Coarse-graining support:

Support.Sobolev.Foundations.CubeNeumannW22CZ.WeakInteriorDQ.QuantCutoffLowerH1

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

theorem HCPolySupport.WeakPoissonEquationOn.directDifferenceQuotient_sqCutoff_energy_quarter_le_two_forcing_sq_add_three_error {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 : ℝ} (hstep : step ≠ 0) (i : Fin d) (hVshift : V ⊆ translateSet (-step • basisVec i) U) {η : Vec d → ℝ} (hη : ContDiff ℝ (↑⊤) η) (hη_compact : HasCompactSupport η) (hη_sub : tsupport η ⊆ V) (hη_abs_le_one : ∀ (x : Vec d), |η x| ≤ 1) : 1 / 4 * ∫ (x : Vec d) in V, η x ^ 2 * vecNormSq ((u.forwardDifferenceQuotientOn step i ⋯ hVU hVshift).grad x) ≤ (2 * ∫ (x : Vec d) in U, f x ^ 2) + 3 * ∫ (x : Vec d) in V, euclideanForwardDifferenceQuotient step i u.toFun x ^ 2 * vecNormSq (euclideanGradient η x)

Absorbed direct squared-cutoff Caccioppoli estimate for the forward difference quotient. This is the closed direct-test form: the only right-hand side terms are the forcing and the usual cutoff-gradient error.

theorem HCPolySupport.WeakPoissonEquationOn.quantitativeCubeCutoff_abs_le_one {d : ℕ} {Q : TriadicCube d} {ρ₁ ρ₂ : ℝ} (η : QuantitativeCubeCutoff Q ρ₁ ρ₂) (x : Vec d) : |η.toFun x| ≤ 1

Quantitative cube cutoffs are bounded by one in absolute value.

theorem HCPolySupport.WeakPoissonEquationOn.vecNormSq_euclideanGradient_le_card_mul_fderiv_norm_sq {d : ℕ} (η : Vec d → ℝ) (x : Vec d) : vecNormSq (euclideanGradient η x) ≤ ↑d * ‖fderiv ℝ η x‖ ^ 2

The squared Euclidean-gradient vector is controlled by the operator norm of the Fréchet derivative, with the explicit finite-dimensional coordinate factor.

theorem HCPolySupport.WeakPoissonEquationOn.vecNormSq_euclideanGradient_quantitativeCubeCutoff_le {d : ℕ} {Q : TriadicCube d} {ρ₁ ρ₂ : ℝ} (η : QuantitativeCubeCutoff Q ρ₁ ρ₂) (x : Vec d) : vecNormSq (euclideanGradient η.toFun x) ≤ ↑d * (quantitativeCubeCutoffGradientConst d / ((ρ₂ - ρ₁) * cubeRadius Q)) ^ 2

Pointwise gradient-error bound for a quantitative cube cutoff.

theorem HCPolySupport.WeakPoissonEquationOn.integral_sq_mul_vecNormSq_euclideanGradient_quantitativeCubeCutoff_le {d : ℕ} {Q : TriadicCube d} {ρ₁ ρ₂ : ℝ} (η : QuantitativeCubeCutoff Q ρ₁ ρ₂) {V : Set (Vec d)} {w : Vec d → ℝ} (hw : MemScalarL2 V w) : ∫ (x : Vec d) in V, w x ^ 2 * vecNormSq (euclideanGradient η.toFun x) ≤ ↑d * (quantitativeCubeCutoffGradientConst d / ((ρ₂ - ρ₁) * cubeRadius Q)) ^ 2 * ∫ (x : Vec d) in V, w x ^ 2

Integral form of the quantitative cube cutoff gradient-error bound.

theorem HCPolySupport.WeakPoissonEquationOn.directDifferenceQuotient_quantitativeCubeCutoff_energy_quarter_le_forcing_sq_add_quotient_sq {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 : ℝ} (hstep : step ≠ 0) (i : Fin d) (hVshift : V ⊆ translateSet (-step • basisVec i) U) {Q : TriadicCube d} {ρ₁ ρ₂ : ℝ} (η : QuantitativeCubeCutoff Q ρ₁ ρ₂) (hη_sub : tsupport η.toFun ⊆ V) : 1 / 4 * ∫ (x : Vec d) in V, η.toFun x ^ 2 * vecNormSq ((u.forwardDifferenceQuotientOn step i ⋯ hVU hVshift).grad x) ≤ (2 * ∫ (x : Vec d) in U, f x ^ 2) + 3 * (↑d * (quantitativeCubeCutoffGradientConst d / ((ρ₂ - ρ₁) * cubeRadius Q)) ^ 2) * ∫ (x : Vec d) in V, euclideanForwardDifferenceQuotient step i u.toFun x ^ 2

Direct Caccioppoli estimate specialized to a quantitative cube cutoff: the cutoff-gradient error is bounded by the explicit inverse-gap squared constant times the unweighted forward quotient square.

theorem HCPolySupport.WeakPoissonEquationOn.integral_vecNormSq_le_integral_sqCutoff_vecNormSq_of_subset_eq_one {d : ℕ} {S V : Set (Vec d)} {G : Vec d → Vec d} {η : Vec d → ℝ} (hS_meas : MeasurableSet S) (hSV : S ⊆ V) (hη_one : ∀ x ∈ S, η x = 1) (hG : MemVectorL2 V G) (hη : ContDiff ℝ (↑⊤) η) (hη_compact : HasCompactSupport η) : ∫ (x : Vec d) in S, vecNormSq (G x) ≤ ∫ (x : Vec d) in V, η x ^ 2 * vecNormSq (G x)

If a cutoff is identically one on an inner measurable set, then its weighted energy over the ambient set controls the unweighted energy on the inner set.

theorem HCPolySupport.WeakPoissonEquationOn.differenceQuotient_innerEnergy_le_forcing_and_quotient {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 : ℝ} (hstep : step ≠ 0) (i : Fin d) (hVshift : V ⊆ translateSet (-step • basisVec i) U) {Q : TriadicCube d} {ρ₁ ρ₂ : ℝ} (η : QuantitativeCubeCutoff Q ρ₁ ρ₂) (hη_sub : tsupport η.toFun ⊆ V) {S : Set (Vec d)} (hS_meas : MeasurableSet S) (hSV : S ⊆ V) (hη_one : ∀ x ∈ S, η.toFun x = 1) : 1 / 4 * ∫ (x : Vec d) in S, vecNormSq ((u.forwardDifferenceQuotientOn step i ⋯ hVU hVshift).grad x) ≤ (2 * ∫ (x : Vec d) in U, f x ^ 2) + 3 * (↑d * (quantitativeCubeCutoffGradientConst d / ((ρ₂ - ρ₁) * cubeRadius Q)) ^ 2) * ∫ (x : Vec d) in V, euclideanForwardDifferenceQuotient step i u.toFun x ^ 2

Quantitative-cube Caccioppoli estimate with the left side localized to any measurable inner set on which the cutoff is identically one.

theorem HCPolySupport.WeakPoissonEquationOn.differenceQuotient_cubeCutoffEnergy_quarter_le_forcingAndQuotientSquares {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 : ℝ} (hstep : step ≠ 0) (i : Fin d) (hVshift : V ⊆ translateSet (-step • basisVec i) U) {Q : TriadicCube d} {ρ₁ ρ₂ : ℝ} (η : QuantitativeCubeCutoff Q ρ₁ ρ₂) (hη_sub : tsupport η.toFun ⊆ V) (hinnerV : scaledClosedCubeSet Q ρ₁ ⊆ V) : 1 / 4 * ∫ (x : Vec d) in scaledClosedCubeSet Q ρ₁, vecNormSq ((u.forwardDifferenceQuotientOn step i ⋯ hVU hVshift).grad x) ≤ (2 * ∫ (x : Vec d) in U, f x ^ 2) + 3 * (↑d * (quantitativeCubeCutoffGradientConst d / ((ρ₂ - ρ₁) * cubeRadius Q)) ^ 2) * ∫ (x : Vec d) in V, euclideanForwardDifferenceQuotient step i u.toFun x ^ 2

Nested-cube version of the quantitative direct Caccioppoli estimate: the inner energy is taken over scaledClosedCubeSet Q ρ₁, where the quantitative cutoff is exactly one.

theorem HCPolySupport.WeakPoissonEquationOn.restrict_test_cutoffForwardDifferenceQuotientToH10 {d : ℕ} {U V : Set (Vec d)} {u : H1Function U} {f : Vec d → ℝ} (h : WeakPoissonEquationOn U u f) (hV : IsOpenBoundedConvexDomain V) (hVU : V ⊆ U) (hfV : MemScalarL2 V f) (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 V, vecDot ((u.restrict ⋯ hVU).grad x) ((u.cutoffForwardDifferenceQuotientToH10 step i hV hVU hVshift hφ hφ_compact hφ_sub).grad x) = ∫ (x : Vec d) in V, f x * (φ x * euclideanForwardDifferenceQuotient step i u.toFun x)

Test a restricted weak Poisson equation against a smooth cutoff times a forward coordinate difference quotient of the solution.

theorem HCPolySupport.WeakPoissonEquationOn.restrict_test_cutoffBackwardDifferenceQuotientToH10 {d : ℕ} {U V : Set (Vec d)} {u : H1Function U} {f : Vec d → ℝ} (h : WeakPoissonEquationOn U u f) (hV : IsOpenBoundedConvexDomain V) (hVU : V ⊆ U) (hfV : MemScalarL2 V f) (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 V, vecDot ((u.restrict ⋯ hVU).grad x) ((u.cutoffBackwardDifferenceQuotientToH10 step i hV hVU hVshift hφ hφ_compact hφ_sub).grad x) = ∫ (x : Vec d) in V, f x * (φ x * euclideanBackwardDifferenceQuotient step i u.toFun x)

Test a restricted weak Poisson equation against a smooth cutoff times a backward coordinate difference quotient of the solution.

theorem HCPolySupport.WeakPoissonEquationOn.test_mulContDiffHasCompactSupportToH10 {d : ℕ} {U : Set (Vec d)} {u : H1Function U} {f : Vec d → ℝ} (h : WeakPoissonEquationOn U u f) (hU : IsOpenBoundedConvexDomain U) (hf : MemScalarL2 U f) {φ : Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hφ_compact : HasCompactSupport φ) (hφ_sub : tsupport φ ⊆ U) : ∫ (x : Vec d) in U, vecDot (u.grad x) ((u.mulContDiffHasCompactSupportToH10 hU hφ hφ_compact hφ_sub).grad x) = ∫ (x : Vec d) in U, f x * (φ x * u.toFun x)

Test a weak Poisson equation against a smooth cutoff times the solution.

theorem HCPolySupport.WeakPoissonEquationOn.mulContDiffHasCompactSupportToH10_grad_coord_ae {d : ℕ} {U : Set (Vec d)} (u : H1Function U) (hU : IsOpenBoundedConvexDomain U) {φ : Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hφ_compact : HasCompactSupport φ) (hφ_sub : tsupport φ ⊆ U) (j : Fin d) : (fun (x : Vec d) => (u.mulContDiffHasCompactSupportToH10 hU hφ hφ_compact hφ_sub).grad x j) =ᵐ[MeasureTheory.volume.restrict U] fun (x : Vec d) => φ x * u.grad x j + u.toFun x * (fderiv ℝ φ x) (basisVec j)

Coordinatewise gradient identification for the chosen H¹₀ representative of a smooth cutoff times an H¹ function.

theorem HCPolySupport.WeakPoissonEquationOn.mulContDiffHasCompactSupportToH10_grad_ae {d : ℕ} {U : Set (Vec d)} (u : H1Function U) (hU : IsOpenBoundedConvexDomain U) {φ : Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hφ_compact : HasCompactSupport φ) (hφ_sub : tsupport φ ⊆ U) : (fun (x : Vec d) => (u.mulContDiffHasCompactSupportToH10 hU hφ hφ_compact hφ_sub).grad x) =ᵐ[MeasureTheory.volume.restrict U] fun (x : Vec d) (j : Fin d) => φ x * u.grad x j + u.toFun x * (fderiv ℝ φ x) (basisVec j)

Vector-valued a.e. gradient identification for a smooth cutoff times an H¹ function, packaged as the chosen H¹₀ representative.

theorem HCPolySupport.WeakPoissonEquationOn.integral_localized_h10_grad_sq_eq_integral_product_rule_grad_sq {d : ℕ} {U : Set (Vec d)} (u : H1Function U) (hU : IsOpenBoundedConvexDomain U) {φ : Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hφ_compact : HasCompactSupport φ) (hφ_sub : tsupport φ ⊆ U) (i : Fin d) : ∫ (x : Vec d) in U, (u.mulContDiffHasCompactSupportToH10 hU hφ hφ_compact hφ_sub).grad x i ^ 2 = ∫ (x : Vec d) in U, (φ x * u.grad x i + u.toFun x * (fderiv ℝ φ x) (basisVec i)) ^ 2

Coordinate energy of the chosen H10 product representative, rewritten by the explicit product-rule gradient.

theorem HCPolySupport.WeakPoissonEquationOn.integral_set_forwardDifferenceQuotient_sq_le_integral_localized_product_rule_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, (φ x * u.grad x i + u.toFun x * (fderiv ℝ φ x) (basisVec i)) ^ 2

Fully expanded lower-order quotient control for a cutoff-localized H¹ function.

theorem HCPolySupport.WeakPoissonEquationOn.integral_product_rule_grad_sq_le_two_integral_cutoff_grad_sq_add_two_integral_value_fderiv_sq {d : ℕ} {U : Set (Vec d)} (u : H1Function U) {φ : Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hφ_compact : HasCompactSupport φ) (i : Fin d) : ∫ (x : Vec d) in U, (φ x * u.grad x i + u.toFun x * (fderiv ℝ φ x) (basisVec i)) ^ 2 ≤ (2 * ∫ (x : Vec d) in U, (φ x * u.grad x i) ^ 2) + 2 * ∫ (x : Vec d) in U, (u.toFun x * (fderiv ℝ φ x) (basisVec i)) ^ 2

The product-rule square is controlled by the two usual square terms.

theorem HCPolySupport.WeakPoissonEquationOn.integral_forwardDifferenceSq_le_two_cutoffGradientSq_add_two_valueDerivativeSq {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 ≤ (2 * ∫ (x : Vec d) in U, (φ x * u.grad x i) ^ 2) + 2 * ∫ (x : Vec d) in U, (u.toFun x * (fderiv ℝ φ x) (basisVec i)) ^ 2

Lower-order quotient control by the two standard localized H¹ terms.

theorem HCPolySupport.WeakPoissonEquationOn.differenceQuotient_cubeCutoff_innerEnergy_quarter_le_forcing_sq_add_lowerH1Terms {d : ℕ} {U V : Set (Vec d)} {u : H1Function U} {f : Vec d → ℝ} (h : WeakPoissonEquationOn U u f) (hU : IsOpenBoundedConvexDomain U) (hf : MemScalarL2 U f) (hV : IsOpenBoundedConvexDomain V) (hVU : V ⊆ U) {step : ℝ} (hstep : step ≠ 0) (i : Fin d) (hVshift : V ⊆ translateSet (-step • basisVec i) U) {Q : TriadicCube d} {ρ₁ ρ₂ : ℝ} (η : QuantitativeCubeCutoff Q ρ₁ ρ₂) (hη_sub : tsupport η.toFun ⊆ V) {S : Set (Vec d)} (hS_meas : MeasurableSet S) (hSV : S ⊆ V) (hη_one : ∀ x ∈ S, η.toFun x = 1) {θ : Vec d → ℝ} (hθ : ContDiff ℝ (↑⊤) θ) (hθ_compact : HasCompactSupport θ) (hθ_sub : tsupport θ ⊆ U) (hθ_one : ∀ x ∈ V, θ x = 1) (hθ_shift_one : ∀ x ∈ V, θ (euclideanCoordShift step i x) = 1) : 1 / 4 * ∫ (x : Vec d) in S, vecNormSq ((u.forwardDifferenceQuotientOn step i ⋯ hVU hVshift).grad x) ≤ (2 * ∫ (x : Vec d) in U, f x ^ 2) + 3 * (↑d * (quantitativeCubeCutoffGradientConst d / ((ρ₂ - ρ₁) * cubeRadius Q)) ^ 2) * ((2 * ∫ (x : Vec d) in U, (θ x * u.grad x i) ^ 2) + 2 * ∫ (x : Vec d) in U, (u.toFun x * (fderiv ℝ θ x) (basisVec i)) ^ 2)

Nested quantitative Caccioppoli with the lower-order quotient term replaced by the two standard localized H¹ terms.

theorem HCPolySupport.WeakPoissonEquationOn.differenceQuotient_cutoffEnergy_le_forcingAndLowerH1Terms {d : ℕ} {U V : Set (Vec d)} {u : H1Function U} {f : Vec d → ℝ} (h : WeakPoissonEquationOn U u f) (hU : IsOpenBoundedConvexDomain U) (hf : MemScalarL2 U f) (hV : IsOpenBoundedConvexDomain V) (hVU : V ⊆ U) {step : ℝ} (hstep : step ≠ 0) (i : Fin d) (hVshift : V ⊆ translateSet (-step • basisVec i) U) {Q : TriadicCube d} {ρ₁ ρ₂ σ₁ σ₂ : ℝ} (η : QuantitativeCubeCutoff Q ρ₁ ρ₂) (hη_sub : tsupport η.toFun ⊆ V) {S : Set (Vec d)} (hS_meas : MeasurableSet S) (hSV : S ⊆ V) (hη_one : ∀ x ∈ S, η.toFun x = 1) (θ : QuantitativeCubeCutoff Q σ₁ σ₂) (hθ_sub : tsupport θ.toFun ⊆ U) (hVθ : V ⊆ scaledClosedCubeSet Q σ₁) (hVshiftθ : ∀ x ∈ V, euclideanCoordShift step i x ∈ scaledClosedCubeSet Q σ₁) : 1 / 4 * ∫ (x : Vec d) in S, vecNormSq ((u.forwardDifferenceQuotientOn step i ⋯ hVU hVshift).grad x) ≤ (2 * ∫ (x : Vec d) in U, f x ^ 2) + 3 * (↑d * (quantitativeCubeCutoffGradientConst d / ((ρ₂ - ρ₁) * cubeRadius Q)) ^ 2) * ((2 * ∫ (x : Vec d) in U, (θ.toFun x * u.grad x i) ^ 2) + 2 * ∫ (x : Vec d) in U, (u.toFun x * (fderiv ℝ θ.toFun x) (basisVec i)) ^ 2)

Nested quantitative Caccioppoli with both the inner and outer cutoffs chosen from the quantitative cube-cutoff package. The outer cutoff is assumed to be identically one on the intermediate domain and on its forward-shifted points.

theorem HCPolySupport.WeakPoissonEquationOn.differenceQuotient_cubeCutoffEnergy_le_forcingAndLowerH1Terms {d : ℕ} {U V : Set (Vec d)} {u : H1Function U} {f : Vec d → ℝ} (h : WeakPoissonEquationOn U u f) (hU : IsOpenBoundedConvexDomain U) (hf : MemScalarL2 U f) (hV : IsOpenBoundedConvexDomain V) (hVU : V ⊆ U) {step : ℝ} (hstep : step ≠ 0) (i : Fin d) (hVshift : V ⊆ translateSet (-step • basisVec i) U) {Q : TriadicCube d} {ρ₁ ρ₂ σ₁ σ₂ : ℝ} (η : QuantitativeCubeCutoff Q ρ₁ ρ₂) (hη_sub : tsupport η.toFun ⊆ V) (hinnerV : scaledClosedCubeSet Q ρ₁ ⊆ V) (θ : QuantitativeCubeCutoff Q σ₁ σ₂) (hθ_sub : tsupport θ.toFun ⊆ U) (hVθ : V ⊆ scaledClosedCubeSet Q σ₁) (hVshiftθ : ∀ x ∈ V, euclideanCoordShift step i x ∈ scaledClosedCubeSet Q σ₁) : 1 / 4 * ∫ (x : Vec d) in scaledClosedCubeSet Q ρ₁, vecNormSq ((u.forwardDifferenceQuotientOn step i ⋯ hVU hVshift).grad x) ≤ (2 * ∫ (x : Vec d) in U, f x ^ 2) + 3 * (↑d * (quantitativeCubeCutoffGradientConst d / ((ρ₂ - ρ₁) * cubeRadius Q)) ^ 2) * ((2 * ∫ (x : Vec d) in U, (θ.toFun x * u.grad x i) ^ 2) + 2 * ∫ (x : Vec d) in U, (u.toFun x * (fderiv ℝ θ.toFun x) (basisVec i)) ^ 2)

Inner-cube version of the nested quantitative Caccioppoli estimate with a quantitative outer lower-order cutoff.

theorem HCPolySupport.WeakPoissonEquationOn.differenceQuotient_cubeCutoffEnergy_le_forcingAndLowerH1Terms_of_step_abs {d : ℕ} {U V : Set (Vec d)} {u : H1Function U} {f : Vec d → ℝ} (h : WeakPoissonEquationOn U u f) (hU : IsOpenBoundedConvexDomain U) (hf : MemScalarL2 U f) (hV : IsOpenBoundedConvexDomain V) (hVU : V ⊆ U) {step : ℝ} (hstep : step ≠ 0) (i : Fin d) (hVshift : V ⊆ translateSet (-step • basisVec i) U) {Q : TriadicCube d} {ρ₁ ρ₂ σ₁ σ₂ ν : ℝ} (η : QuantitativeCubeCutoff Q ρ₁ ρ₂) (hη_sub : tsupport η.toFun ⊆ V) (hinnerV : scaledClosedCubeSet Q ρ₁ ⊆ V) (θ : QuantitativeCubeCutoff Q σ₁ σ₂) (hθ_sub : tsupport θ.toFun ⊆ U) (hVν : V ⊆ scaledClosedCubeSet Q ν) (hνσ : ν ≤ σ₁) (hstep_abs : |step| ≤ (σ₁ - ν) * cubeRadius Q) : 1 / 4 * ∫ (x : Vec d) in scaledClosedCubeSet Q ρ₁, vecNormSq ((u.forwardDifferenceQuotientOn step i ⋯ hVU hVshift).grad x) ≤ (2 * ∫ (x : Vec d) in U, f x ^ 2) + 3 * (↑d * (quantitativeCubeCutoffGradientConst d / ((ρ₂ - ρ₁) * cubeRadius Q)) ^ 2) * ((2 * ∫ (x : Vec d) in U, (θ.toFun x * u.grad x i) ^ 2) + 2 * ∫ (x : Vec d) in U, (u.toFun x * (fderiv ℝ θ.toFun x) (basisVec i)) ^ 2)

Inner-cube nested quantitative Caccioppoli with the outer shifted-containment hypothesis discharged by a one-coordinate step-size restriction.

theorem HCPolySupport.WeakPoissonEquationOn.differenceQuotient_openCubeCutoffEnergy_le_forcingAndLowerH1Terms {d : ℕ} {V : Set (Vec d)} {Q : TriadicCube d} {uQ : H1Function (openCubeSet Q)} {f : Vec d → ℝ} (h : WeakPoissonEquationOn (openCubeSet Q) uQ f) (hf : MemScalarL2 (openCubeSet Q) f) (hV : IsOpenBoundedConvexDomain V) {step : ℝ} (hstep : step ≠ 0) (i : Fin d) {ρ₁ ρ₂ σ₁ σ₂ ν : ℝ} (η : QuantitativeCubeCutoff Q ρ₁ ρ₂) (hη_sub : tsupport η.toFun ⊆ V) (hinnerV : scaledClosedCubeSet Q ρ₁ ⊆ V) (θ : QuantitativeCubeCutoff Q σ₁ σ₂) (hVν : V ⊆ scaledClosedCubeSet Q ν) (hν_nonneg : 0 ≤ ν) (hνσ : ν ≤ σ₁) (hσ₁_lt_one : σ₁ < 1) (hσ₂_nonneg : 0 ≤ σ₂) (hσ₂_lt_one : σ₂ < 1) (hstep_abs : |step| ≤ (σ₁ - ν) * cubeRadius Q) : 1 / 4 * ∫ (x : Vec d) in scaledClosedCubeSet Q ρ₁, vecNormSq ((uQ.forwardDifferenceQuotientOn step i ⋯ ⋯ ⋯).grad x) ≤ (2 * ∫ (x : Vec d) in openCubeSet Q, f x ^ 2) + 3 * (↑d * (quantitativeCubeCutoffGradientConst d / ((ρ₂ - ρ₁) * cubeRadius Q)) ^ 2) * ((2 * ∫ (x : Vec d) in openCubeSet Q, (θ.toFun x * uQ.grad x i) ^ 2) + 2 * ∫ (x : Vec d) in openCubeSet Q, (uQ.toFun x * (fderiv ℝ θ.toFun x) (basisVec i)) ^ 2)

Open-cube ambient version of the nested quantitative Caccioppoli estimate: the ambient-domain containment, shifted containment, and outer cutoff support are all discharged by strict subcube radii and the step-size bound.