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 Homogenization.Bornology.IsBounded.isBoundedDomain {d : ℕ} {U : Set (Vec d)} (hU : Bornology.IsBounded U) : IsBoundedDomain U

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

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

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

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

theorem Homogenization.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 Homogenization.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 Homogenization.IsOpenBoundedConvexDomain {d : ℕ} (U : Set (Vec d)) : Prop

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

Equations

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

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

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

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

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

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

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

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

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

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

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

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

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

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