Coarse-graining support:

Support.Sobolev.Foundations.CubeNeumannW22CZ.WeakInteriorDQ.SmoothTestBoundEstimate

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

theorem HCPolySupport.WeakPoissonEquationOn.setIntegral_openCubeSet_cutoff_grad_sq_le {d : ℕ} {Q : TriadicCube d} (uQ : H1Function (openCubeSet Q)) (i : Fin d) {σ₁ σ₂ : ℝ} (θ : QuantitativeCubeCutoff Q σ₁ σ₂) : ∫ (x : Vec d) in openCubeSet Q, (θ.toFun x * uQ.grad x i) ^ 2 ≤ ∫ (x : Vec d) in openCubeSet Q, uQ.grad x i ^ 2

Multiplication by a quantitative cube cutoff does not increase a single gradient-coordinate square integral.

theorem HCPolySupport.WeakPoissonEquationOn.sq_fderiv_quantitativeCubeCutoff_apply_basisVec_le {d : ℕ} {Q : TriadicCube d} {σ₁ σ₂ : ℝ} (θ : QuantitativeCubeCutoff Q σ₁ σ₂) (i : Fin d) (x : Vec d) : (fderiv ℝ θ.toFun x) (basisVec i) ^ 2 ≤ ↑d * (quantitativeCubeCutoffGradientConst d / ((σ₂ - σ₁) * cubeRadius Q)) ^ 2

A coordinate derivative of a quantitative cube cutoff is bounded by the finite-dimensional cutoff-gradient constant.

theorem HCPolySupport.WeakPoissonEquationOn.setIntegral_openCubeSet_value_fderiv_cutoff_sq_le {d : ℕ} {Q : TriadicCube d} (uQ : H1Function (openCubeSet Q)) (i : Fin d) {σ₁ σ₂ : ℝ} (θ : QuantitativeCubeCutoff Q σ₁ σ₂) : ∫ (x : Vec d) in openCubeSet Q, (uQ.toFun x * (fderiv ℝ θ.toFun x) (basisVec i)) ^ 2 ≤ ↑d * (quantitativeCubeCutoffGradientConst d / ((σ₂ - σ₁) * cubeRadius Q)) ^ 2 * ∫ (x : Vec d) in openCubeSet Q, uQ.toFun x ^ 2

The cutoff-derivative lower-order term is controlled by the L² size of the function and the explicit finite-dimensional cutoff-gradient constant.

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

A reduced version of the smooth-test quotient-Hessian bound where the two cutoff lower-order terms have been replaced by unweighted H¹ integrals.

Equations

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

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

The smooth-test quotient-Hessian bound is controlled by its reduced unweighted H¹ version.