Coarse-graining support:

Support.Sobolev.Foundations.CubeNeumannW22CZ.WeakInteriorDQ.ScaledCoerciveDepth

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

Scale-correct coercivity constants for C.2 depth estimates

This file plugs the dilation-scaled cube Poincare estimate into the scale-sharp Hessian-to-Besov depth handoff. The main point is that all depth-j descendants of a triadic cube have the same scale, so the prefactor volume(R)^{-1/2} * PoincareConstant(R) is uniform over descendants.

noncomputable def HCPolySupport.scaledDescendantMeanZeroH1CoerciveEstimate {d : ℕ} (Q : TriadicCube d) (j : ℕ) (R : TriadicCube d) : R ∈ descendantsAtDepth Q j → H1CoerciveEstimate (openCubeSet R)

The scaled mean-zero coercivity estimate on every depth-j descendant.

Equations

• HCPolySupport.scaledDescendantMeanZeroH1CoerciveEstimate Q j R _hR = HCPolySupport.scaledTranslatedCubeMeanZeroH1CoerciveEstimate R

noncomputable def HCPolySupport.scaledDescendantCoercivePrefactor {d : ℕ} (Q : TriadicCube d) (j : ℕ) : ℝ

Uniform depth constant for the scale-sharp C.2 Poincare prefactor.

Equations

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

theorem HCPolySupport.scaledDescendantCoercivePrefactor_nonneg {d : ℕ} (Q : TriadicCube d) (j : ℕ) : 0 ≤ scaledDescendantCoercivePrefactor Q j

theorem HCPolySupport.scaledDescendantCoercivePrefactor_eq {d : ℕ} {Q R : TriadicCube d} {j : ℕ} (hR : R ∈ descendantsAtDepth Q j) : (cubeVolume R)⁻¹ ^ (1 / 2) * (scaledDescendantMeanZeroH1CoerciveEstimate Q j R hR).constantValue = scaledDescendantCoercivePrefactor Q j

theorem HCPolySupport.scaledDescendantCoercivePrefactor_bound {d : ℕ} {Q R : TriadicCube d} {j : ℕ} (hR : R ∈ descendantsAtDepth Q j) : (cubeVolume R)⁻¹ ^ (1 / 2) * (scaledDescendantMeanZeroH1CoerciveEstimate Q j R hR).constantValue ≤ scaledDescendantCoercivePrefactor Q j

theorem HCPolySupport.cubeBesovDepthWeight_mul_scaledDescendantCoercivePrefactor {d : ℕ} (Q : TriadicCube d) (j : ℕ) : cubeBesovDepthWeight Q 1 j * scaledDescendantCoercivePrefactor Q j = (cubeVolume (originCube d (Q.scale - ↑j)))⁻¹ ^ (1 / 2) * (originCubeMeanZeroH1CoerciveEstimate d 0).constantValue

theorem HCPolySupport.scaledDepthPrefactor_mul_cardInvHessianRoot_eq_parentVolume {d : ℕ} (Q : TriadicCube d) (j : ℕ) {A : ℝ} (hA : 0 ≤ A) : cubeBesovDepthWeight Q 1 j * (scaledDescendantCoercivePrefactor Q j * ((↑(descendantsAtDepth Q j).card)⁻¹ * A ^ 2) ^ (1 / 2)) = (cubeVolume Q)⁻¹ ^ (1 / 2) * (originCubeMeanZeroH1CoerciveEstimate d 0).constantValue * A

theorem HCPolySupport.HasWeakHessianOn.cubeBesovDepthSeminorm_gradCoord_le_depthWeight_mul_scaledCoercivePrefactor {d : ℕ} {Q : TriadicCube d} {u : H1Function (openCubeSet Q)} (H : HasWeakHessianOn (openCubeSet Q) u) (i : Fin d) (j : ℕ) : cubeBesovDepthSeminorm Q 1 2 (fun (x : Vec d) => u.grad x i) j ≤ cubeBesovDepthWeight Q 1 j * (scaledDescendantCoercivePrefactor Q j * ((↑(descendantsAtDepth Q j).card)⁻¹ * H.hessianCoordL2NormSum ^ 2) ^ (1 / 2))

Scale-correct C.2 depth handoff with the descendant Poincare constants discharged by dilation-scaled cube coercivity.

theorem HCPolySupport.HasWeakHessianOn.cubeBesovDepthSeminorm_gradCoord_le_parentVolume_scaledCoercive {d : ℕ} {Q : TriadicCube d} {u : H1Function (openCubeSet Q)} (H : HasWeakHessianOn (openCubeSet Q) u) (i : Fin d) (j : ℕ) : cubeBesovDepthSeminorm Q 1 2 (fun (x : Vec d) => u.grad x i) j ≤ (cubeVolume Q)⁻¹ ^ (1 / 2) * (originCubeMeanZeroH1CoerciveEstimate d 0).constantValue * H.hessianCoordL2NormSum