Geometry for ball Poincare estimates

Adapted from CoarseGraining (LeanIntoHomogenization, 2026) with the author's permission. This file keeps the bounded convex-domain and affine-segment interfaces needed by the ball estimate while using the established CKN carriers.

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

A coordinatewise bounded domain in the native finite-dimensional carrier.

Equations

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

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

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

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

noncomputable def CKN.integralAverage {d : ℕ} (U : Set (Vec d)) (u : Vec d → ℝ) : ℝ

The average of a scalar function over a restricted volume measure.

Equations

• CKN.integralAverage U u = MeasureTheory.average (MeasureTheory.volume.restrict U) u

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

Measurable bounded domain on which the Sobolev estimates are formulated.

Equations

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

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

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

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

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

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

An open bounded convex domain in the native carrier.

Equations

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

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

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

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

theorem CKN.IsOpenBoundedConvexDomain.measurableSet {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) : MeasurableSet U

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

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

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

theorem CKN.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

def CKN.translateSet {d : ℕ} (z : Vec d) (U : Set (Vec d)) : Set (Vec d)

Translate a set by a vector in the native finite-dimensional carrier.

Equations

• CKN.translateSet z U = {x : CKN.Vec d | ∃ y ∈ U, x = y + z}

theorem CKN.mem_translateSet_iff_sub_mem {d : ℕ} {z x : Vec d} {U : Set (Vec d)} : x ∈ translateSet z U ↔ x - z ∈ U

theorem CKN.preimage_addNeg_eq_translateSet {d : ℕ} (z : Vec d) (U : Set (Vec d)) : (fun (x : Vec d) => x + -z) ⁻¹' U = translateSet z U

theorem CKN.translateSet_translateSet {d : ℕ} (z w : Vec d) (U : Set (Vec d)) : translateSet w (translateSet z U) = translateSet (z + w) U

@[simp]

theorem CKN.translateSet_zero {d : ℕ} (U : Set (Vec d)) : translateSet 0 U = U

theorem CKN.measurePreserving_subRight_restrict_translateSet {d : ℕ} (z : Vec d) (U : Set (Vec d)) : MeasureTheory.MeasurePreserving (fun (x : Vec d) => x - z) (MeasureTheory.volume.restrict (translateSet z U)) (MeasureTheory.volume.restrict U)

theorem CKN.image_addRight_eq_translateSet {d : ℕ} (z : Vec d) (U : Set (Vec d)) : (fun (x : Vec d) => x + z) '' U = translateSet z U

theorem CKN.measurePreserving_addRight_restrict_translateSet {d : ℕ} (z : Vec d) (U : Set (Vec d)) : MeasureTheory.MeasurePreserving (fun (x : Vec d) => x + z) (MeasureTheory.volume.restrict U) (MeasureTheory.volume.restrict (translateSet z U))

theorem CKN.setIntegral_comp_subRight_translateSet {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (z : Vec d) (U : Set (Vec d)) (f : Vec d → E) : ∫ (x : Vec d) in translateSet z U, f (x - z) = ∫ (y : Vec d) in U, f y

theorem CKN.setIntegral_comp_addRight_translateSet {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (z : Vec d) (U : Set (Vec d)) (f : Vec d → E) : ∫ (y : Vec d) in U, f (y + z) = ∫ (x : Vec d) in translateSet z U, f x

theorem CKN.isOpenBoundedConvexDomain_ball {d : ℕ} (x₀ : Vec d) {r : ℝ} (hr : 0 < r) : IsOpenBoundedConvexDomain (Metric.ball x₀ r)

def CKN.ballAffineMap {d : ℕ} (x₀ : Vec d) (r : ℝ) (x : Vec d) : Vec d

The affine map which sends the unit ball to the ball of radius r.

Equations

• CKN.ballAffineMap x₀ r x = x₀ + r • x

noncomputable def CKN.segmentBlend {d : ℕ} (x : Vec d) (t : ℝ) (y : Vec d) : Vec d

The point on the segment from y to x with parameter t.

Equations

• CKN.segmentBlend x t y = (AffineMap.lineMap y x) t

@[simp]

theorem CKN.segmentBlend_zero {d : ℕ} (x y : Vec d) : segmentBlend x 0 y = y

@[simp]

theorem CKN.segmentBlend_one {d : ℕ} (x y : Vec d) : segmentBlend x 1 y = x

theorem CKN.segmentBlend_eq_add_smul_sub {d : ℕ} (x y : Vec d) (t : ℝ) : segmentBlend x t y = y + t • (x - y)

@[simp]

theorem CKN.segmentBlend_self {d : ℕ} (x : Vec d) (t : ℝ) : segmentBlend x t x = x

theorem CKN.segmentBlend_mem {d : ℕ} {U : Set (Vec d)} (hU : Convex ℝ U) {x y : Vec d} (hx : x ∈ U) (hy : y ∈ U) {t : ℝ} (ht0 : 0 ≤ t) (ht1 : t ≤ 1) : segmentBlend x t y ∈ U

theorem CKN.segmentBlend_mem_of_isOpenBoundedConvexDomain {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) {x y : Vec d} (hx : x ∈ U) (hy : y ∈ U) {t : ℝ} (ht0 : 0 ≤ t) (ht1 : t ≤ 1) : segmentBlend x t y ∈ U