Coarse-graining support: Support.Sobolev.Foundations.CubeCoerciveH1

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

theorem HCPolySupport.openCubeSet_originCube_eq_smul_unit (d : ℕ) (m : ℤ) : openCubeSet (originCube d m) = cubeScaleFactor (originCube d m) • openCubeSet (originCube d 0)

A centered triadic cube is the dilation of the unit centered cube by its side length.

theorem HCPolySupport.isBoundedDomain_openCubeSet_originCube_scale (d : ℕ) (m : ℤ) : IsBoundedDomain (openCubeSet (originCube d m))

Centered cubes have an explicit coordinate bound by their side length.

theorem HCPolySupport.isOpenBoundedConvexDomain_openCubeSet_originCube_scale (d : ℕ) (m : ℤ) : IsOpenBoundedConvexDomain (openCubeSet (originCube d m))

Centered cubes as bounded open convex domains, with the explicit side-length coordinate bound above.

noncomputable def HCPolySupport.originCubeMeanZeroH1CoerciveEstimate (d : ℕ) (m : ℤ) : H1CoerciveEstimate (openCubeSet (originCube d m))

The bounded-open-convex mean-zero H¹ coercive estimate on a centered triadic cube.

Equations

• HCPolySupport.originCubeMeanZeroH1CoerciveEstimate d m = HCPolySupport.h1CoerciveEstimateOfOpenBoundedConvexDomain ⋯

theorem HCPolySupport.originCubeMeanZeroH1CoerciveEstimate_constant_le_chosenBound (d : ℕ) (m : ℤ) : (originCubeMeanZeroH1CoerciveEstimate d m).constantValue ≤ H1Function.h1CoerciveEstimateChosenBound ⋯

noncomputable def HCPolySupport.translatedCubeMeanZeroH1CoerciveEstimate {d : ℕ} (Q : TriadicCube d) : H1CoerciveEstimate (openCubeSet Q)

A cube coercive estimate obtained by proving Poincare on the centered cube at the same scale and translating it to the target cube. This avoids any dependence on the target cube's location.

Equations

• HCPolySupport.translatedCubeMeanZeroH1CoerciveEstimate Q = { constantValue := (HCPolySupport.originCubeMeanZeroH1CoerciveEstimate d Q.scale).constantValue, constant_nonneg := ⋯, bound := ⋯ }

theorem HCPolySupport.translatedCubeMeanZeroH1CoerciveEstimate_constant {d : ℕ} (Q : TriadicCube d) : (translatedCubeMeanZeroH1CoerciveEstimate Q).constantValue = (originCubeMeanZeroH1CoerciveEstimate d Q.scale).constantValue

theorem HCPolySupport.translatedCubeMeanZeroH1CoerciveEstimate_constant_nonneg {d : ℕ} (Q : TriadicCube d) : 0 ≤ (translatedCubeMeanZeroH1CoerciveEstimate Q).constantValue

theorem HCPolySupport.translatedCubeMeanZeroH1CoerciveEstimate_constant_le_origin_chosenBound {d : ℕ} (Q : TriadicCube d) : (translatedCubeMeanZeroH1CoerciveEstimate Q).constantValue ≤ H1Function.h1CoerciveEstimateChosenBound ⋯

noncomputable def HCPolySupport.scaledOriginCubeMeanZeroH1CoerciveEstimate (d : ℕ) (m : ℤ) : H1CoerciveEstimate (openCubeSet (originCube d m))

Scale-correct coercive estimate on a centered cube, obtained by dilating the unit centered cube estimate.

Equations

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

theorem HCPolySupport.scaledOriginCubeMeanZeroH1CoerciveEstimate_constant (d : ℕ) (m : ℤ) : (scaledOriginCubeMeanZeroH1CoerciveEstimate d m).constantValue = cubeScaleFactor (originCube d m) * (originCubeMeanZeroH1CoerciveEstimate d 0).constantValue

noncomputable def HCPolySupport.scaledTranslatedCubeMeanZeroH1CoerciveEstimate {d : ℕ} (Q : TriadicCube d) : H1CoerciveEstimate (openCubeSet Q)

Scale-correct coercive estimate on any triadic cube, obtained by dilating the unit centered cube and then translating to the target cube.

Equations

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

theorem HCPolySupport.scaledTranslatedCubeMeanZeroH1CoerciveEstimate_constant {d : ℕ} (Q : TriadicCube d) : (scaledTranslatedCubeMeanZeroH1CoerciveEstimate Q).constantValue = cubeScaleFactor Q * (originCubeMeanZeroH1CoerciveEstimate d 0).constantValue