Coarse-graining support: Support.Sobolev.Foundations.AxisCube

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

Axis-aligned cube domains

An axis cube z + (0,L)^d is the open box obtained by translating the product of the open intervals (0,L) by a corner point z. This file records that these boxes fit the ambient Sobolev geometry API: they are open, bounded, convex, and hence open bounded convex domains. These are the reference domains for the interior harmonic estimates.

def HCPolySupport.axisCube {d : ℕ} (z : Vec d) (L : ℝ) : Set (Vec d)

The open axis cube z + (0,L)^d.

Equations

• HCPolySupport.axisCube z L = Set.univ.pi fun (j : Fin d) => Set.Ioo (z j) (z j + L)

theorem HCPolySupport.isOpen_axisCube {d : ℕ} (z : Vec d) (L : ℝ) : IsOpen (axisCube z L)

Axis cubes are open finite products of open intervals.

theorem HCPolySupport.isBoundedDomain_axisCube {d : ℕ} (z : Vec d) (L : ℝ) : IsBoundedDomain (axisCube z L)

Axis cubes are bounded, even in the degenerate or empty cases.

theorem HCPolySupport.convex_axisCube {d : ℕ} (z : Vec d) (L : ℝ) : Convex ℝ (axisCube z L)

Axis cubes are convex finite products of convex intervals.

theorem HCPolySupport.isOpenBoundedConvexDomain_axisCube {d : ℕ} (z : Vec d) (L : ℝ) : IsOpenBoundedConvexDomain (axisCube z L)

Axis cubes are bounded open convex domains in the Sobolev geometry API.