Domain

Support for the Armstrong–Vicol anomalous-diffusion formalization.

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

Coordinatewise boundedness of a spatial domain within a positive-radius box.

Equations

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

def Homogenization.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

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

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

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