Coarse-graining support: Support.Geometry.ConvexDomain

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

Bounded Open Convex Domains

This file bridges the repository's custom bounded-domain predicate IsBoundedDomain with Mathlib's bounded-set API, records the resulting finite measure consequences for Lebesgue measure, and packages the domain class IsOpenBoundedConvexDomain.

The intended analytic use is to give future Sobolev/Hodge results a stable geometric target class that already contains the open cubes and metric balls used downstream.

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

theorem HCPolySupport.IsBoundedDomain.isBounded {d : ℕ} {U : Set (Vec d)} (hU : IsBoundedDomain U) : Bornology.IsBounded U

theorem HCPolySupport.IsBoundedDomain.volume_lt_top {d : ℕ} {U : Set (Vec d)} (hU : IsBoundedDomain U) : MeasureTheory.volume U < ⊤

theorem HCPolySupport.IsBoundedDomain.isFiniteMeasure_restrict_volume {d : ℕ} {U : Set (Vec d)} (hU : IsBoundedDomain U) : MeasureTheory.IsFiniteMeasure (MeasureTheory.volume.restrict U)

theorem HCPolySupport.IsBoundedDomain.norm_le_choose {d : ℕ} {U : Set (Vec d)} (hU : IsBoundedDomain U) {x : Vec d} (hx : x ∈ U) : ‖x‖ ≤ Classical.choose hU

theorem HCPolySupport.IsBoundedDomain.norm_sub_le_two_mul_choose {d : ℕ} {U : Set (Vec d)} (hU : IsBoundedDomain U) {x y : Vec d} (hx : x ∈ U) (hy : y ∈ U) : ‖x - y‖ ≤ 2 * Classical.choose hU

theorem HCPolySupport.IsBoundedDomain.rayParameter_le_two_mul_choose_of_mem_of_norm_eq_one {d : ℕ} {U : Set (Vec d)} (hU : IsBoundedDomain U) {x ω : Vec d} {s : ℝ} (hx : x ∈ U) (hs : x + s • ω ∈ U) (hs0 : 0 ≤ s) (hω : ‖ω‖ = 1) : s ≤ 2 * Classical.choose hU

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

Bounded open convex domains in the ambient space Vec d = Fin d → ℝ.

Equations

• HCPolySupport.IsOpenBoundedConvexDomain U = (IsOpen U ∧ HCPolySupport.IsBoundedDomain U ∧ Convex ℝ U)

theorem HCPolySupport.IsOpenBoundedConvexDomain.isOpen {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) : IsOpen U

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

theorem HCPolySupport.IsOpenBoundedConvexDomain.convex {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) : Convex ℝ U

theorem HCPolySupport.IsOpenBoundedConvexDomain.volume_lt_top {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) : MeasureTheory.volume U < ⊤

theorem HCPolySupport.IsOpenBoundedConvexDomain.isFiniteMeasure_restrict_volume {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) : MeasureTheory.IsFiniteMeasure (MeasureTheory.volume.restrict U)

theorem HCPolySupport.IsOpenBoundedConvexDomain.isSobolevRegularDomain {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) : IsSobolevRegularDomain U

theorem HCPolySupport.IsOpenBoundedConvexDomain.translateSet {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (z : Vec d) : IsOpenBoundedConvexDomain (HCPolySupport.translateSet z U)

theorem HCPolySupport.IsSobolevRegularDomain.volume_lt_top {d : ℕ} {U : Set (Vec d)} (hU : IsSobolevRegularDomain U) : MeasureTheory.volume U < ⊤

theorem HCPolySupport.IsSobolevRegularDomain.isFiniteMeasure_restrict_volume {d : ℕ} {U : Set (Vec d)} (hU : IsSobolevRegularDomain U) : MeasureTheory.IsFiniteMeasure (MeasureTheory.volume.restrict U)

theorem HCPolySupport.isOpenBoundedConvexDomain_ball {d : ℕ} (x : Vec d) {r : ℝ} (_hr : 0 < r) : IsOpenBoundedConvexDomain (Metric.ball x r)

theorem HCPolySupport.isBoundedDomain_openCubeSet {d : ℕ} (Q : TriadicCube d) : IsBoundedDomain (openCubeSet Q)

theorem HCPolySupport.convex_openCubeSet {d : ℕ} (Q : TriadicCube d) : Convex ℝ (openCubeSet Q)

theorem HCPolySupport.isOpenBoundedConvexDomain_openCubeSet {d : ℕ} (Q : TriadicCube d) : IsOpenBoundedConvexDomain (openCubeSet Q)