High-contrast homogenization: Analytic.ConvexDomains

Imported from the Apache-2.0 HighContrastHomogenization development at commit 7a13dbcd8d6609264a713373f5c69ceeac870472.

Bounded open convex domains and the ball sandwich

The Dirichlet estimate e.random.dirichlet is stated on a domain, and the shape datum a domain carries here is a ball sandwich: concentric Euclidean balls of radii ρ and Rad inside and outside it, HasBallSandwich U ρ Rad.

The first two sections exhibit the sandwich for the two domains that occur, the ambient supremum-norm ball and the Euclidean ball, and show that the Euclidean ball is a bounded open convex domain in the sense of the coarse-graining library. The third shows that this class is stable under images by an invertible matrix and produces, for every invertible M and every radius r > 0, a nonempty bounded open convex domain whose M-image carries the tight sandwich (r, r). The last two sections record the measure-theoretic consequences of the domain class and the sanity facts about the two radii.

The ball sandwich of the ambient (sup-norm) ball

theorem HCPolySupport.HighContrast.hasBallSandwich_metricBall {d : ℕ} (c : Vec d) {r : ℝ} (hr : 0 < r) (hd : 0 < d) : HasBallSandwich (Metric.ball c r) r (r * √↑d)

The sup-norm ball of Vec d is sandwiched between concentric Euclidean balls of radii r and r * √d. The hypothesis 0 < d is necessary: for d = 0 the sup-ball is the whole (one-point) space while euclideanBallAt c (r * √0) = euclideanBallAt c 0 = ∅.

theorem HCPolySupport.HighContrast.hasBallSandwich_metricBall_succ {d : ℕ} (c : Vec d) {r : ℝ} (hr : 0 < r) : HasBallSandwich (Metric.ball c r) r (r * √(↑d + 1))

The dimension-uniform version of the sandwich for the sup-norm ball, with the slightly larger outer radius r * √(d + 1); no positivity hypothesis on the dimension is needed.

The Euclidean ball is a bounded open convex domain

theorem HCPolySupport.HighContrast.convex_euclideanBallAt {d : ℕ} (c : Vec d) (r : ℝ) : Convex ℝ (euclideanBallAt c r)

theorem HCPolySupport.HighContrast.isBoundedDomain_euclideanBallAt {d : ℕ} (c : Vec d) {r : ℝ} (hr : 0 < r) : IsBoundedDomain (euclideanBallAt c r)

theorem HCPolySupport.HighContrast.isOpenBoundedConvexDomain_euclideanBallAt {d : ℕ} (c : Vec d) {r : ℝ} (hr : 0 < r) : IsOpenBoundedConvexDomain (euclideanBallAt c r)

The Euclidean ball is a bounded open convex domain in the sense of the coarse-graining library.

theorem HCPolySupport.HighContrast.hasBallSandwich_euclideanBallAt {d : ℕ} (c : Vec d) {r : ℝ} (hr : 0 < r) : HasBallSandwich (euclideanBallAt c r) r r

The tight ball sandwich: the Euclidean ball of radius r is its own inner and outer ball.

Linear images

theorem HCPolySupport.HighContrast.mem_matImage_iff {d : ℕ} {M : Mat d} {U : Set (Vec d)} (y : Vec d) : y ∈ matImage M U ↔ ∃ x ∈ U, matVecMul M x = y

theorem HCPolySupport.HighContrast.matImage_eq_preimage {d : ℕ} {M : Mat d} (hM : IsUnit (Matrix.det M)) (U : Set (Vec d)) : matImage M U = (fun (y : Vec d) => matVecMul M⁻¹ y) ⁻¹' U

For an invertible M, the linear image is the preimage under the inverse.

theorem HCPolySupport.HighContrast.isOpen_matImage {d : ℕ} {M : Mat d} (hM : IsUnit (Matrix.det M)) {U : Set (Vec d)} (hU : IsOpen U) : IsOpen (matImage M U)

theorem HCPolySupport.HighContrast.convex_matImage {d : ℕ} {M : Mat d} {U : Set (Vec d)} (hU : Convex ℝ U) : Convex ℝ (matImage M U)

theorem HCPolySupport.HighContrast.isBoundedDomain_matImage {d : ℕ} {M : Mat d} {U : Set (Vec d)} (hU : IsBoundedDomain U) : IsBoundedDomain (matImage M U)

theorem HCPolySupport.HighContrast.isOpenBoundedConvexDomain_matImage {d : ℕ} {M : Mat d} {U : Set (Vec d)} (hM : IsUnit (Matrix.det M)) (hU : IsOpenBoundedConvexDomain U) : IsOpenBoundedConvexDomain (matImage M U)

The linear image of a bounded open convex domain under an invertible matrix is again a bounded open convex domain.

theorem HCPolySupport.HighContrast.matImage_matImage_inv {d : ℕ} {M : Mat d} (hM : IsUnit (Matrix.det M)) (S : Set (Vec d)) : matImage M (matImage M⁻¹ S) = S

theorem HCPolySupport.HighContrast.nonempty_matImage {d : ℕ} {M : Mat d} {U : Set (Vec d)} (hU : U.Nonempty) : (matImage M U).Nonempty

Domains carrying a prescribed ball sandwich

For an invertible M and any r > 0 there is a nonempty bounded open convex domain whose M-image is exactly the Euclidean ball of radius r, hence carries the tight ball sandwich (r, r). This is two of the three domain conditions the Dirichlet estimate imposes; the third, containment in the unit ellipsoid, is supplied separately, and only the two together inhabit that estimate.

theorem HCPolySupport.HighContrast.exists_domain_with_ballSandwich {d : ℕ} {M : Mat d} (hM : IsUnit (Matrix.det M)) {r : ℝ} (hr : 0 < r) : ∃ (U : Set (Vec d)), IsOpenBoundedConvexDomain U ∧ U.Nonempty ∧ HasBallSandwich (matImage M U) r r

Structural consequences of the domain class

IsOpenBoundedConvexDomain.volume_lt_top, .isSobolevRegularDomain and .isFiniteMeasure_restrict_volume already exist in the coarse-graining library; the only missing piece is positivity of the volume, which needs nonemptiness.

theorem HCPolySupport.HighContrast.measurableSet_of_isOpenBoundedConvexDomain {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) : MeasurableSet U

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

theorem HCPolySupport.HighContrast.volume_pos_of_isOpenBoundedConvexDomain {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (hne : U.Nonempty) : 0 < MeasureTheory.volume U

theorem HCPolySupport.HighContrast.volume_ne_zero_of_isOpenBoundedConvexDomain {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (hne : U.Nonempty) : MeasureTheory.volume U ≠ 0

theorem HCPolySupport.HighContrast.volume_ne_top_of_isOpenBoundedConvexDomain {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) : MeasureTheory.volume U ≠ ⊤

Sanity facts about the ball sandwich

euclideanBallAt c r depends on r only through r ^ 2, so the inclusions alone cannot distinguish a radius from its negative; that is why the sign of each radius is a field of the predicate. With the signs fixed, the inner radius does not exceed the outer one in positive dimension.

theorem HCPolySupport.HighContrast.euclideanBallAt_abs {d : ℕ} (c : Vec d) (r : ℝ) : euclideanBallAt c |r| = euclideanBallAt c r

theorem HCPolySupport.HighContrast.HasBallSandwich.abs_radii {d : ℕ} {U : Set (Vec d)} {ρ Rad : ℝ} (h : HasBallSandwich U ρ Rad) : |ρ| = ρ ∧ |Rad| = Rad

The radii of a sandwich are their own absolute values.

theorem HCPolySupport.HighContrast.HasBallSandwich.le_abs_of_pos_dim {d : ℕ} {U : Set (Vec d)} {ρ Rad : ℝ} (hd : 0 < d) (h : HasBallSandwich U ρ Rad) (hρ : 0 < ρ) : ρ ≤ |Rad|

The inner radius of a sandwich never exceeds the outer radius in absolute value, in positive dimension.

theorem HCPolySupport.HighContrast.HasBallSandwich.le_of_pos_dim {d : ℕ} {U : Set (Vec d)} {ρ Rad : ℝ} (hd : 0 < d) (h : HasBallSandwich U ρ Rad) : ρ ≤ Rad

With the signs fixed by the predicate, the inner radius of a sandwich does not exceed the outer radius.