Coarse-graining support: Support.Geometry.OriginCubeMeasureBridge

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

theorem HCPolySupport.cubeSet_originCube_ae_eq_openCubeSet {d : ℕ} (n : ℤ) : cubeSet (originCube d n) =ᵐ[MeasureTheory.volume] openCubeSet (originCube d n)

The half-open and open realizations of the centered cube at scale n agree almost everywhere for Lebesgue measure.

theorem HCPolySupport.volume_restrict_cubeSet_originCube_eq_volume_restrict_openCubeSet_originCube {d : ℕ} (n : ℤ) : MeasureTheory.volume.restrict (cubeSet (originCube d n)) = MeasureTheory.volume.restrict (openCubeSet (originCube d n))

Restricted Lebesgue measure on the half-open centered cube agrees with the restriction to the corresponding open cube.

theorem HCPolySupport.ae_restrict_cubeSet_originCube_iff {d : ℕ} {n : ℤ} {p : Vec d → Prop} : (∀ᵐ (x : Vec d) ∂MeasureTheory.volume.restrict (cubeSet (originCube d n)), p x) ↔ ∀ᵐ (x : Vec d) ∂MeasureTheory.volume.restrict (openCubeSet (originCube d n)), p x

Almost-everywhere statements over the half-open centered cube are equivalent to the corresponding statements over the open centered cube.

theorem HCPolySupport.integrableOn_cubeSet_originCube_iff_integrableOn_openCubeSet_originCube {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] {n : ℤ} {f : Vec d → E} : MeasureTheory.IntegrableOn f (cubeSet (originCube d n)) MeasureTheory.volume ↔ MeasureTheory.IntegrableOn f (openCubeSet (originCube d n)) MeasureTheory.volume

Integrability on the half-open centered cube is equivalent to integrability on the corresponding open cube.

theorem HCPolySupport.setIntegral_cubeSet_originCube_eq_setIntegral_openCubeSet_originCube {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℤ} {f : Vec d → E} : ∫ (x : Vec d) in cubeSet (originCube d n), f x = ∫ (x : Vec d) in openCubeSet (originCube d n), f x

Set integrals over the half-open centered cube and the corresponding open cube agree.