Coarse-graining support:

Support.Sobolev.Foundations.CubeNeumannW22CZ.WeakInteriorDQ.ReflectionGeometry

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

theorem HCPolySupport.scaledOpenCubeSet_originCube_succ_one_div_three (d : ℕ) (m : ℤ) : scaledOpenCubeSet (originCube d (m + 1)) (1 / 3) = openCubeSet (originCube d m)

The centered cube of scale m is the one-third scaled open subcube of the centered cube at the next larger scale. This is the basic geometry behind using an all-face reflection block as an interior domain after translating to the centered cube.

theorem HCPolySupport.cubeFaceReflectionBlockSet_originCube_subset_openCubeSet_succ (d : ℕ) (m : ℤ) : cubeFaceReflectionBlockSet (originCube d m) ⊆ openCubeSet (originCube d (m + 1))

The centered all-face reflection block of originCube d m lies inside the centered cube at the next larger scale. The reverse inclusion only fails on the internal reflecting faces.

theorem HCPolySupport.ae_forall_ne_originCube_reflection_faces (d : ℕ) (m : ℤ) : ∀ᵐ (x : Vec d), ∀ (i : Fin d), x i ≠ -(1 / 2) * 3 ^ m ∧ x i ≠ 1 / 2 * 3 ^ m

Almost every point avoids the two internal reflecting faces of the centered reflection block in every coordinate.

theorem HCPolySupport.cubeFaceReflectionBlockSet_originCube_ae_eq_openCubeSet_succ (d : ℕ) (m : ℤ) : cubeFaceReflectionBlockSet (originCube d m) =ᵐ[MeasureTheory.volume] openCubeSet (originCube d (m + 1))

The centered all-face reflection block is the next larger centered open cube modulo the null union of internal reflecting faces.

theorem HCPolySupport.setIntegral_openCubeSet_succ_originCube_eq_cubeFaceReflectionBlockSet {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (m : ℤ) (f : Vec d → E) : ∫ (x : Vec d) in openCubeSet (originCube d (m + 1)), f x = ∫ (x : Vec d) in cubeFaceReflectionBlockSet (originCube d m), f x

Set integrals over the next larger centered open cube can be evaluated on the centered reflection block, since the two domains differ only by internal faces.