Coarse-graining support: Support.Geometry.Domain

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

def HCPolySupport.IsBoundedDomain {d : ℕ} (U : Set (Vec d)) : Prop

The domain lies in a coordinate box of some positive finite radius.

Equations

• HCPolySupport.IsBoundedDomain U = ∃ (R : ℝ), 0 < R ∧ ∀ x ∈ U, ∀ (i : Fin d), |x i| ≤ R

def HCPolySupport.IsSobolevRegularDomain {d : ℕ} (U : Set (Vec d)) : Prop

Working domain-regularity predicate for the current Sobolev layer.

At this stage of the development, the reusable geometric input needed by the mean-zero and affine-average arguments is exactly measurability together with the repository's bounded-domain predicate.

Equations

• HCPolySupport.IsSobolevRegularDomain U = (MeasurableSet U ∧ HCPolySupport.IsBoundedDomain U)

theorem HCPolySupport.IsSobolevRegularDomain.measurableSet {d : ℕ} {U : Set (Vec d)} (hU : IsSobolevRegularDomain U) : MeasurableSet U

theorem HCPolySupport.IsSobolevRegularDomain.isBoundedDomain {d : ℕ} {U : Set (Vec d)} (hU : IsSobolevRegularDomain U) : IsBoundedDomain U