Coarse-graining support:

Support.Sobolev.Foundations.CubeNeumannW22CZ.WeakInteriorDQ.InnerCubeAndHessian

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

theorem HCPolySupport.WeakPoissonEquationOn.abs_neg_integral_forwardDifferenceQuotient_mul_fderiv_openCube_innerCube_le_of_step_abs_le {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 j : 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) {φ : Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hφ_compact : HasCompactSupport φ) (hφ_sub_inner : tsupport φ ⊆ scaledClosedCubeSet Q ρ₁) : |(-∫ (x : Vec d) in V, euclideanForwardDifferenceQuotient step i uQ.toFun x * (fderiv ℝ φ x) (basisVec j))| ≤ 2 * ((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)) + 1 / 2 * ∫ (x : Vec d) in scaledClosedCubeSet Q ρ₁, φ x ^ 2

Open-cube quantitative test-functional bound obtained by combining the inner-cube Caccioppoli estimate with the weak-gradient handoff. This is the uniform small-step form aimed at the weak Hessian limit argument.

theorem HCPolySupport.WeakPoissonEquationOn.neg_integral_forwardDifference_mul_derivative_innerCube_le_energyRoot_l2Bound {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 j : 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) {φ : Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hφ_compact : HasCompactSupport φ) (hφ_sub_inner : tsupport φ ⊆ scaledClosedCubeSet Q ρ₁) : |(-∫ (x : Vec d) in V, euclideanForwardDifferenceQuotient step i uQ.toFun x * (fderiv ℝ φ x) (basisVec j))| ≤ (4 * ((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))) ^ (1 / 2) * (∫ (x : Vec d) in scaledClosedCubeSet Q ρ₁, ‖φ x‖ ^ 2) ^ (1 / 2)

Open-cube homogeneous test-functional bound obtained by combining the inner-cube Caccioppoli estimate with the full-gradient Cauchy handoff.

theorem HCPolySupport.WeakPoissonEquationOn.neg_integral_forwardDifference_mul_derivative_openCube_innerCube_eq_zero {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 j : 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) {φ : Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hφ_compact : HasCompactSupport φ) (hφ_sub_inner : tsupport φ ⊆ scaledClosedCubeSet Q ρ₁) (hφ_zero : ∫ (x : Vec d) in scaledClosedCubeSet Q ρ₁, ‖φ x‖ ^ 2 = 0) : -∫ (x : Vec d) in V, euclideanForwardDifferenceQuotient step i uQ.toFun x * (fderiv ℝ φ x) (basisVec j) = 0

Open-cube version of the zero-seminorm well-definedness consequence for the quotient Hessian test functional.

theorem HCPolySupport.WeakPoissonEquationOn.neg_integral_forwardDifference_mul_derivative_openCube_innerCube_eq_of_step_abs {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 j : 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) {φ ψ : Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hψ : ContDiff ℝ (↑⊤) ψ) (hφ_compact : HasCompactSupport φ) (hψ_compact : HasCompactSupport ψ) (hφ_sub_inner : tsupport φ ⊆ scaledClosedCubeSet Q ρ₁) (hψ_sub_inner : tsupport ψ ⊆ scaledClosedCubeSet Q ρ₁) (hφψ_zero : ∫ (x : Vec d) in scaledClosedCubeSet Q ρ₁, ‖φ x - ψ x‖ ^ 2 = 0) : -∫ (x : Vec d) in V, euclideanForwardDifferenceQuotient step i uQ.toFun x * (fderiv ℝ φ x) (basisVec j) = -∫ (x : Vec d) in V, euclideanForwardDifferenceQuotient step i uQ.toFun x * (fderiv ℝ ψ x) (basisVec j)

Open-cube version of the distance-zero well-definedness consequence for the quotient Hessian test functional.

theorem HCPolySupport.WeakPoissonEquationOn.neg_integral_forwardDifference_mul_derivative_openCube_innerCube_eq {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 j : 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) (φ ψ : H1WeakTestFunction (scaledClosedCubeSet Q ρ₁)) (hφψ : φ.toScalarL2 = ψ.toScalarL2) : -∫ (x : Vec d) in V, euclideanForwardDifferenceQuotient step i uQ.toFun x * (fderiv ℝ φ.toFun x) (basisVec j) = -∫ (x : Vec d) in V, euclideanForwardDifferenceQuotient step i uQ.toFun x * (fderiv ℝ ψ.toFun x) (basisVec j)

The open-cube quotient-Hessian pairing depends only on the scalar L² class of a smooth weak test on the inner cube.

noncomputable def HCPolySupport.WeakPoissonEquationOn.openCubeInnerQuotientHessianSmoothTestBound {d : ℕ} {Q : TriadicCube d} (uQ : H1Function (openCubeSet Q)) (f : Vec d → ℝ) (i : Fin d) {ρ₁ ρ₂ σ₁ σ₂ : ℝ} (θ : QuantitativeCubeCutoff Q σ₁ σ₂) : ℝ

The explicit square-root bound controlling the smooth-test quotient-Hessian functional on an inner cube.

Equations

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

noncomputable def HCPolySupport.WeakPoissonEquationOn.openCubeInnerQuotientHessianSmoothTestFunctional {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 j : 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) : ↥(h1WeakTestScalarL2Submodule (scaledClosedCubeSet Q ρ₁)) →ₗ[ℝ] ℝ

The concrete linear functional on the dense smooth-test ScalarL2 submodule induced by one quotient-Hessian pairing.

Equations

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

theorem HCPolySupport.WeakPoissonEquationOn.norm_openCubeInnerQuotientHessianSmoothTestFunctional_apply_le {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 j : 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) (x : ↥(h1WeakTestScalarL2Submodule (scaledClosedCubeSet Q ρ₁))) : ‖(h.openCubeInnerQuotientHessianSmoothTestFunctional hf hV hstep i j η hη_sub hinnerV θ hVν hν_nonneg hνσ hσ₁_lt_one hσ₂_nonneg hσ₂_lt_one hstep_abs) x‖ ≤ openCubeInnerQuotientHessianSmoothTestBound uQ f i θ * ‖(h1WeakTestScalarL2Submodule (scaledClosedCubeSet Q ρ₁)).subtype x‖

The concrete smooth-test functional satisfies the square-root operator bound needed by the dense-domain extension API.

theorem HCPolySupport.WeakPoissonEquationOn.test_mulContDiffHasCompactSupport_expanded {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) fun (j : Fin d) => φ x * u.grad x j + u.toFun x * (fderiv ℝ φ x) (basisVec j)) = ∫ (x : Vec d) in U, f x * (φ x * u.toFun x)

Product-rule form of the cutoff energy test.

theorem HCPolySupport.WeakPoissonEquationOn.cutoffForwardDifferenceQuotientToH10_grad_coord_ae {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) : (fun (x : Vec d) => (u.cutoffForwardDifferenceQuotientToH10 step i hV hVU hVshift hφ hφ_compact hφ_sub).grad x j) =ᵐ[MeasureTheory.volume.restrict V] fun (x : Vec d) => φ x * (u.forwardDifferenceQuotientOn step i ⋯ hVU hVshift).grad x j + euclideanForwardDifferenceQuotient step i u.toFun x * (fderiv ℝ φ x) (basisVec j)

Coordinatewise gradient identification for the forward localized difference-quotient test. The H¹₀ constructor is chosen through membership data, so the product-rule gradient is recovered by weak-derivative uniqueness on the open interior domain.

theorem HCPolySupport.WeakPoissonEquationOn.cutoffBackwardDifferenceQuotientToH10_grad_coord_ae {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) : (fun (x : Vec d) => (u.cutoffBackwardDifferenceQuotientToH10 step i hV hVU hVshift hφ hφ_compact hφ_sub).grad x j) =ᵐ[MeasureTheory.volume.restrict V] fun (x : Vec d) => φ x * (u.backwardDifferenceQuotientOn step i ⋯ hVU hVshift).grad x j + euclideanBackwardDifferenceQuotient step i u.toFun x * (fderiv ℝ φ x) (basisVec j)

Coordinatewise gradient identification for the backward localized difference-quotient test.

theorem HCPolySupport.WeakPoissonEquationOn.cutoffForwardDifferenceQuotientToH10_grad_ae {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) : (fun (x : Vec d) => (u.cutoffForwardDifferenceQuotientToH10 step i hV hVU hVshift hφ hφ_compact hφ_sub).grad x) =ᵐ[MeasureTheory.volume.restrict V] fun (x : Vec d) (j : Fin d) => φ x * (u.forwardDifferenceQuotientOn step i ⋯ hVU hVshift).grad x j + euclideanForwardDifferenceQuotient step i u.toFun x * (fderiv ℝ φ x) (basisVec j)

Vector-valued a.e. gradient identification for the forward localized difference-quotient test.

theorem HCPolySupport.WeakPoissonEquationOn.cutoffBackwardDifferenceQuotientToH10_grad_ae {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) : (fun (x : Vec d) => (u.cutoffBackwardDifferenceQuotientToH10 step i hV hVU hVshift hφ hφ_compact hφ_sub).grad x) =ᵐ[MeasureTheory.volume.restrict V] fun (x : Vec d) (j : Fin d) => φ x * (u.backwardDifferenceQuotientOn step i ⋯ hVU hVshift).grad x j + euclideanBackwardDifferenceQuotient step i u.toFun x * (fderiv ℝ φ x) (basisVec j)

Vector-valued a.e. gradient identification for the backward localized difference-quotient test.

theorem HCPolySupport.WeakPoissonEquationOn.restrict_test_cutoffForwardDifferenceQuotient_expanded {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) fun (j : Fin d) => φ x * (u.forwardDifferenceQuotientOn step i ⋯ hVU hVshift).grad x j + euclideanForwardDifferenceQuotient step i u.toFun x * (fderiv ℝ φ x) (basisVec j)) = ∫ (x : Vec d) in V, f x * (φ x * euclideanForwardDifferenceQuotient step i u.toFun x)

Expanded weak-test identity for a forward localized difference quotient. This is the product-rule form of restrict_test_cutoffForwardDifferenceQuotientToH10.

theorem HCPolySupport.WeakPoissonEquationOn.restrict_test_cutoffBackwardDifferenceQuotient_expanded {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) fun (j : Fin d) => φ x * (u.backwardDifferenceQuotientOn step i ⋯ hVU hVshift).grad x j + euclideanBackwardDifferenceQuotient step i u.toFun x * (fderiv ℝ φ x) (basisVec j)) = ∫ (x : Vec d) in V, f x * (φ x * euclideanBackwardDifferenceQuotient step i u.toFun x)

Expanded weak-test identity for a backward localized difference quotient.