Coarse-graining support:

Support.Sobolev.Foundations.CubeNeumannW22CZ.WeakInteriorDQ.ScaledCubeGeometry

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

theorem HCPolySupport.scaledClosedCubeSet_subset_scaledOpenCubeSet_of_lt {d : ℕ} (Q : TriadicCube d) {ρ σ : ℝ} (hρσ : ρ < σ) : scaledClosedCubeSet Q ρ ⊆ scaledOpenCubeSet Q σ

A closed concentric cube of smaller relative radius lies in the open concentric cube of any strictly larger relative radius.

theorem HCPolySupport.ball_cubeCenter_mul_cubeRadius_eq_scaledOpenCubeSet {d : ℕ} (Q : TriadicCube d) {ρ : ℝ} (hρ : 0 < ρ) : Metric.ball (cubeCenter Q) (ρ * cubeRadius Q) = scaledOpenCubeSet Q ρ

Positive scaled open cubes are metric balls for the sup metric on Vec d.

theorem HCPolySupport.isOpenBoundedConvexDomain_scaledOpenCubeSet_of_pos {d : ℕ} (Q : TriadicCube d) {ρ : ℝ} (hρ : 0 < ρ) : IsOpenBoundedConvexDomain (scaledOpenCubeSet Q ρ)

Positive scaled open cubes are admissible open bounded convex domains.