Coarse-graining support: Support.Geometry.OverlapCube

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

noncomputable def HCPolySupport.ScalarOverlap.scaleFactor {d : ℕ} (S : TriadicCube d) : ℝ

Side length of the overlapping cube centered at the fine-grid cube S. If S has scale k - 1, this overlapping cube has side length 3^k.

Equations

• HCPolySupport.ScalarOverlap.scaleFactor S = 3 * HCPolySupport.cubeScaleFactor S

theorem HCPolySupport.ScalarOverlap.scaleFactor_pos {d : ℕ} (S : TriadicCube d) : 0 < scaleFactor S

theorem HCPolySupport.ScalarOverlap.scaleFactor_nonneg {d : ℕ} (S : TriadicCube d) : 0 ≤ scaleFactor S

def HCPolySupport.ScalarOverlap.cubeSet {d : ℕ} (S : TriadicCube d) : Set (Vec d)

The half-open overlapping cube centered at cubeCenter S with side length 3 * cubeScaleFactor S.

Equations

• One or more equations did not get rendered due to their size.

def HCPolySupport.ScalarOverlap.openCubeSet {d : ℕ} (S : TriadicCube d) : Set (Vec d)

The open overlapping cube with the same center and side length as cubeSet.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.ScalarOverlap.measurableSet_coord_halfOpenStrip {d : ℕ} (i : Fin d) (a b : ℝ) : MeasurableSet {x : Vec d | a ≤ x i ∧ x i < b}

theorem HCPolySupport.ScalarOverlap.measurableSet_coord_openStrip {d : ℕ} (i : Fin d) (a b : ℝ) : MeasurableSet {x : Vec d | a < x i ∧ x i < b}

theorem HCPolySupport.ScalarOverlap.measurableSet_cubeSet {d : ℕ} (S : TriadicCube d) : MeasurableSet (cubeSet S)

theorem HCPolySupport.ScalarOverlap.measurableSet_openCubeSet {d : ℕ} (S : TriadicCube d) : MeasurableSet (openCubeSet S)

theorem HCPolySupport.ScalarOverlap.isOpen_openCubeSet {d : ℕ} (S : TriadicCube d) : IsOpen (openCubeSet S)

theorem HCPolySupport.ScalarOverlap.cubeSet_eq_pi_Ico {d : ℕ} (S : TriadicCube d) : cubeSet S = Set.univ.pi fun (i : Fin d) => Set.Ico ((↑(S.index i) - 3 / 2) * cubeScaleFactor S) ((↑(S.index i) + 3 / 2) * cubeScaleFactor S)

theorem HCPolySupport.ScalarOverlap.openCubeSet_eq_pi_Ioo {d : ℕ} (S : TriadicCube d) : openCubeSet S = Set.univ.pi fun (i : Fin d) => Set.Ioo ((↑(S.index i) - 3 / 2) * cubeScaleFactor S) ((↑(S.index i) + 3 / 2) * cubeScaleFactor S)

theorem HCPolySupport.ScalarOverlap.cubeSet_ae_eq_openCubeSet {d : ℕ} (S : TriadicCube d) : cubeSet S =ᵐ[MeasureTheory.volume] openCubeSet S

theorem HCPolySupport.ScalarOverlap.volume_restrict_cubeSet_eq_volume_restrict_openCubeSet {d : ℕ} (S : TriadicCube d) : MeasureTheory.volume.restrict (cubeSet S) = MeasureTheory.volume.restrict (openCubeSet S)

theorem HCPolySupport.ScalarOverlap.openCubeSet_subset_cubeSet {d : ℕ} (S : TriadicCube d) : openCubeSet S ⊆ cubeSet S

theorem HCPolySupport.ScalarOverlap.interior_cubeSet_eq_openCubeSet {d : ℕ} (Q : TriadicCube d) : interior (HCPolySupport.cubeSet Q) = HCPolySupport.openCubeSet Q

def HCPolySupport.ScalarOverlap.middleChildCube {d : ℕ} (Q : TriadicCube d) : TriadicCube d

The central triadic child of Q, with scale decreased by one and each index multiplied by three.

Equations

• HCPolySupport.ScalarOverlap.middleChildCube Q = { scale := Q.scale - 1, index := fun (i : Fin d) => 3 * Q.index i }

theorem HCPolySupport.ScalarOverlap.middleChildCube_mem_childCubes {d : ℕ} (Q : TriadicCube d) : middleChildCube Q ∈ childCubes Q

@[simp]

theorem HCPolySupport.ScalarOverlap.scaleFactor_middleChildCube {d : ℕ} (Q : TriadicCube d) : scaleFactor (middleChildCube Q) = cubeScaleFactor Q

theorem HCPolySupport.ScalarOverlap.cubeSet_middleChildCube_eq_cubeSet {d : ℕ} (Q : TriadicCube d) : cubeSet (middleChildCube Q) = HCPolySupport.cubeSet Q

theorem HCPolySupport.ScalarOverlap.cubeSet_middleChildCube_subset_cubeSet {d : ℕ} (Q : TriadicCube d) : cubeSet (middleChildCube Q) ⊆ HCPolySupport.cubeSet Q

theorem HCPolySupport.ScalarOverlap.middleChildCube_injective {d : ℕ} : Function.Injective middleChildCube

noncomputable def HCPolySupport.ScalarOverlap.cubeVolume {d : ℕ} (S : TriadicCube d) : ℝ

Volume of an overlapping cube.

Equations

• HCPolySupport.ScalarOverlap.cubeVolume S = HCPolySupport.ScalarOverlap.scaleFactor S ^ d

@[simp]

theorem HCPolySupport.ScalarOverlap.cubeVolume_middleChildCube {d : ℕ} (Q : TriadicCube d) : cubeVolume (middleChildCube Q) = HCPolySupport.cubeVolume Q

theorem HCPolySupport.ScalarOverlap.cubeVolume_pos {d : ℕ} (S : TriadicCube d) : 0 < cubeVolume S

theorem HCPolySupport.ScalarOverlap.cubeVolume_nonneg {d : ℕ} (S : TriadicCube d) : 0 ≤ cubeVolume S

@[simp]

theorem HCPolySupport.ScalarOverlap.volume_cubeSet_toReal {d : ℕ} (S : TriadicCube d) : (MeasureTheory.volume (cubeSet S)).toReal = cubeVolume S

@[simp]

theorem HCPolySupport.ScalarOverlap.volume_openCubeSet_toReal {d : ℕ} (S : TriadicCube d) : (MeasureTheory.volume (openCubeSet S)).toReal = cubeVolume S

theorem HCPolySupport.ScalarOverlap.volume_cubeSet_lt_top {d : ℕ} (S : TriadicCube d) : MeasureTheory.volume (cubeSet S) < ⊤

noncomputable def HCPolySupport.ScalarOverlap.cubeMeasure {d : ℕ} (S : TriadicCube d) : MeasureTheory.Measure (Vec d)

Unnormalized measure on an overlapping cube.

Equations

• HCPolySupport.ScalarOverlap.cubeMeasure S = MeasureTheory.volume.restrict (HCPolySupport.ScalarOverlap.cubeSet S)

noncomputable def HCPolySupport.ScalarOverlap.normalizedCubeMeasure {d : ℕ} (S : TriadicCube d) : MeasureTheory.Measure (Vec d)

Normalized measure on an overlapping cube.

Equations

• HCPolySupport.ScalarOverlap.normalizedCubeMeasure S = ENNReal.ofReal (HCPolySupport.ScalarOverlap.cubeVolume S)⁻¹ • HCPolySupport.ScalarOverlap.cubeMeasure S

@[simp]

theorem HCPolySupport.ScalarOverlap.cubeMeasure_apply_univ {d : ℕ} (S : TriadicCube d) : (cubeMeasure S) Set.univ = MeasureTheory.volume (cubeSet S)

theorem HCPolySupport.ScalarOverlap.cubeMeasure_apply_univ_toReal {d : ℕ} (S : TriadicCube d) : ((cubeMeasure S) Set.univ).toReal = cubeVolume S

theorem HCPolySupport.ScalarOverlap.cubeMeasure_apply_univ_ne_top {d : ℕ} (S : TriadicCube d) : (cubeMeasure S) Set.univ ≠ ⊤

theorem HCPolySupport.ScalarOverlap.cubeMeasure_apply_univ_eq {d : ℕ} (S : TriadicCube d) : (cubeMeasure S) Set.univ = ENNReal.ofReal (cubeVolume S)

@[simp]

theorem HCPolySupport.ScalarOverlap.normalizedCubeMeasure_apply_univ {d : ℕ} (S : TriadicCube d) : (normalizedCubeMeasure S) Set.univ = 1

instance HCPolySupport.ScalarOverlap.normalizedCubeMeasure.instIsFiniteMeasure {d : ℕ} (S : TriadicCube d) : MeasureTheory.IsFiniteMeasure (normalizedCubeMeasure S)

theorem HCPolySupport.ScalarOverlap.normalizedCubeMeasure_ne_zero {d : ℕ} (S : TriadicCube d) : normalizedCubeMeasure S ≠ 0

theorem HCPolySupport.ScalarOverlap.lintegral_normalizedCubeMeasure_eq {d : ℕ} (S : TriadicCube d) (f : Vec d → ENNReal) : ∫⁻ (x : Vec d), f x ∂normalizedCubeMeasure S = ENNReal.ofReal (cubeVolume S)⁻¹ * ∫⁻ (x : Vec d) in cubeSet S, f x