Documentation

LeanPool.HighContrastHomogenization.Provider.Regularity.CubeVolume

High-contrast homogenization: Provider.Regularity.CubeVolume #

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

Cube volumes are nonzero and finite #

The two corollaries of the exact cube-volume formula that every domain-change estimate on a triadic cube needs: an open cube has volume neither 0 nor ⊤. Both follow at once from volume_openCubeSet_toReal and the positivity of the cube's scale factor. They are collected here so that the estimates consuming them share one statement instead of repeating the argument.

source
theorem HCPolySupport.HighContrast.volume_openCubeSet_ne_zero {d : ℕ} (Q : TriadicCube d) :
MeasureTheory.volume (openCubeSet Q) ≠ 0

An open triadic cube has nonzero volume.

source
theorem HCPolySupport.HighContrast.volume_openCubeSet_ne_top {d : ℕ} (Q : TriadicCube d) :
MeasureTheory.volume (openCubeSet Q) ≠ ⊤

An open triadic cube has finite volume.