Coarse-graining support: Support.Multiscale.NormalizedDomainCube

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

Triadic cubes as bounded measurable domains

This module packages the operational half-open carrier of a triadic cube as a BoundedMeasurableDomain. The source-facing open cube remains only almost-everywhere equal to this carrier; no equality of the two sets is used or claimed here.

noncomputable def HCPolySupport.cubeBoundedMeasurableDomain {d : ℕ} (Q : TriadicCube d) : BoundedMeasurableDomain d

The half-open carrier of a triadic cube, packaged with its geometric regularity and positive volume.

Equations

• HCPolySupport.cubeBoundedMeasurableDomain Q = { carrier := HCPolySupport.cubeSet Q, measurableSet := ⋯, isBoundedDomain := ⋯, volume_pos := ⋯ }

@[simp]

theorem HCPolySupport.coe_cubeBoundedMeasurableDomain {d : ℕ} (Q : TriadicCube d) : ↑(cubeBoundedMeasurableDomain Q) = cubeSet Q

@[simp]

theorem HCPolySupport.cubeBoundedMeasurableDomain_restrictedVolume_eq_cubeMeasure {d : ℕ} (Q : TriadicCube d) : (cubeBoundedMeasurableDomain Q).restrictedVolume = cubeMeasure Q

Restricting volume to the safe cube domain is exactly the existing cube measure.

theorem HCPolySupport.cubeBoundedMeasurableDomain_normalizedVolume_eq_normalizedCubeMeasure {d : ℕ} (Q : TriadicCube d) : (cubeBoundedMeasurableDomain Q).normalizedVolume = normalizedCubeMeasure Q

The safe-domain normalization agrees exactly with the established normalized cube measure.

theorem HCPolySupport.cubeBoundedMeasurableDomain_restrictedVolume_eq_restrict_openCubeSet {d : ℕ} (Q : TriadicCube d) : (cubeBoundedMeasurableDomain Q).restrictedVolume = MeasureTheory.volume.restrict (openCubeSet Q)

The operational half-open cube and the source-facing open cube induce the same restricted volume measure.

theorem HCPolySupport.ae_cubeBoundedMeasurableDomain_restrictedVolume_iff_openCubeSet {d : ℕ} (Q : TriadicCube d) {p : Vec d → Prop} : (∀ᵐ (x : Vec d) ∂(cubeBoundedMeasurableDomain Q).restrictedVolume, p x) ↔ ∀ᵐ (x : Vec d) ∂MeasureTheory.volume.restrict (openCubeSet Q), p x

Almost-everywhere statements for the safe cube domain can equivalently be read over the source-facing open cube.

theorem HCPolySupport.cubeBoundedMeasurableDomain_average_eq_cubeAverage {d : ℕ} (Q : TriadicCube d) (f : Vec d → ℝ) (hf : MeasureTheory.Integrable f (cubeBoundedMeasurableDomain Q).restrictedVolume) : (cubeBoundedMeasurableDomain Q).average f hf = cubeAverage Q f

The proof-carrying safe-domain average is the existing cube average.

theorem HCPolySupport.cubeBoundedMeasurableDomain_average_eq_openCubeSet_average {d : ℕ} (Q : TriadicCube d) (f : Vec d → ℝ) (hf : MeasureTheory.Integrable f (cubeBoundedMeasurableDomain Q).restrictedVolume) : (cubeBoundedMeasurableDomain Q).average f hf = (MeasureTheory.volume (openCubeSet Q)).toReal⁻¹ * ∫ (x : Vec d) in openCubeSet Q, f x

The safe-domain average has the source-facing open-cube formula. This is an a.e. bridge, rather than an assertion that the two cube carriers coincide.