Coarse-graining support: Support.Geometry.BoundedConvexDomain

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

Open bounded convex domain adapters

This module keeps the repository's existing set-based predicate IsOpenBoundedConvexDomain U as the domain carrier. Given a nonempty carrier, it supplies the positive-volume bounded measurable domain and open-set adapters needed by normalized and Sobolev constructions.

noncomputable def HCPolySupport.IsOpenBoundedConvexDomain.toBoundedMeasurableDomain {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (hne : U.Nonempty) : BoundedMeasurableDomain d

A nonempty open bounded convex set is a bounded measurable domain of strictly positive Lebesgue volume.

Equations

• hU.toBoundedMeasurableDomain hne = { carrier := U, measurableSet := ⋯, isBoundedDomain := ⋯, volume_pos := ⋯ }

@[simp]

theorem HCPolySupport.IsOpenBoundedConvexDomain.coe_toBoundedMeasurableDomain {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (hne : U.Nonempty) : ↑(hU.toBoundedMeasurableDomain hne) = U

def HCPolySupport.IsOpenBoundedConvexDomain.toOpens {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) : TopologicalSpace.Opens (Vec d)

The open-set carrier associated with an open bounded convex domain.

Equations

• hU.toOpens = { carrier := U, is_open' := ⋯ }

@[simp]

theorem HCPolySupport.IsOpenBoundedConvexDomain.coe_toOpens {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) : ↑hU.toOpens = U