Documentation

LeanPool.HighContrastHomogenization.Support.Geometry.CubeMeasure

Coarse-graining support: Support.Geometry.CubeMeasure #

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

theorem HCPolySupport.measurableSet_cubeSet {d : ℕ} (Q : TriadicCube d) :

MeasurableSet (cubeSet Q)

theorem HCPolySupport.measurableSet_openCubeSet {d : ℕ} (Q : TriadicCube d) :

MeasurableSet (openCubeSet Q)

theorem HCPolySupport.measurableSet_cubeBoundary {d : ℕ} (Q : TriadicCube d) :

MeasurableSet (cubeBoundary Q)

theorem HCPolySupport.measurableSet_cubeShrunkSet {d : ℕ} (Q : TriadicCube d) (t : ℝ) :

MeasurableSet (cubeShrunkSet Q t)

theorem HCPolySupport.measurableSet_cubeBoundaryLayer {d : ℕ} (Q : TriadicCube d) (t : ℝ) :

MeasurableSet (cubeBoundaryLayer Q t)

theorem HCPolySupport.cubeSet_eq_pi_Ico {d : ℕ} (Q : TriadicCube d) :

cubeSet Q = Set.univ.pi fun (i : Fin d) => Set.Ico ((↑(Q.index i) - 1 / 2) * cubeScaleFactor Q) ((↑(Q.index i) + 1 / 2) * cubeScaleFactor Q)

theorem HCPolySupport.openCubeSet_eq_pi_Ioo {d : ℕ} (Q : TriadicCube d) :

openCubeSet Q = Set.univ.pi fun (i : Fin d) => Set.Ioo ((↑(Q.index i) - 1 / 2) * cubeScaleFactor Q) ((↑(Q.index i) + 1 / 2) * cubeScaleFactor Q)

theorem HCPolySupport.cubeShrunkSet_eq_pi_Ico {d : ℕ} (Q : TriadicCube d) (t : ℝ) :

cubeShrunkSet Q t = Set.univ.pi fun (i : Fin d) => Set.Ico ((↑(Q.index i) - 1 / 2 + t) * cubeScaleFactor Q) ((↑(Q.index i) + 1 / 2 - t) * cubeScaleFactor Q)

theorem HCPolySupport.cubeSet_ae_eq_openCubeSet {d : ℕ} (Q : TriadicCube d) :

cubeSet Q =ᵐ[MeasureTheory.volume] openCubeSet Q

theorem HCPolySupport.volume_restrict_cubeSet_eq_volume_restrict_openCubeSet {d : ℕ} (Q : TriadicCube d) :

MeasureTheory.volume.restrict (cubeSet Q) = MeasureTheory.volume.restrict (openCubeSet Q)

theorem HCPolySupport.ae_restrict_cubeSet_iff {d : ℕ} {Q : TriadicCube d} {p : Vec d → Prop} :

(∀ᵐ (x : Vec d) ∂MeasureTheory.volume.restrict (cubeSet Q), p x) ↔ ∀ᵐ (x : Vec d) ∂MeasureTheory.volume.restrict (openCubeSet Q), p x

theorem HCPolySupport.ae_eq_cubeSet_of_mem_descendantsAtDepth_of_ae_eq_openCubeSet {d : ℕ} {Q R : TriadicCube d} {j : ℕ} {α : Type u_1} {f g : Vec d → α} (hR : R ∈ descendantsAtDepth Q j) (hfg : f =ᵐ[MeasureTheory.volume.restrict (openCubeSet Q)] g) :

f =ᵐ[MeasureTheory.volume.restrict (cubeSet R)] g

theorem HCPolySupport.volume_cubeBoundary_le_cubeSet {d : ℕ} (Q : TriadicCube d) :

MeasureTheory.volume (cubeBoundary Q) ≤ MeasureTheory.volume (cubeSet Q)

theorem HCPolySupport.cubeVolume_eq_scaleFactor_pow {d : ℕ} (Q : TriadicCube d) :

cubeVolume Q = cubeScaleFactor Q ^ d

theorem HCPolySupport.cubeVolume_eq_pow_scale {d : ℕ} (Q : TriadicCube d) :

cubeVolume Q = (3 ^ Q.scale) ^ d

@[simp]

theorem HCPolySupport.volume_cubeSet_toReal {d : ℕ} (Q : TriadicCube d) :

(MeasureTheory.volume (cubeSet Q)).toReal = cubeVolume Q

@[simp]

theorem HCPolySupport.volume_openCubeSet_toReal {d : ℕ} (Q : TriadicCube d) :

(MeasureTheory.volume (openCubeSet Q)).toReal = cubeVolume Q

theorem HCPolySupport.volume_cubeShrunkSet_toReal_of_le_half {d : ℕ} (Q : TriadicCube d) {t : ℝ} (ht : t ≤ 1 / 2) :

(MeasureTheory.volume (cubeShrunkSet Q t)).toReal = ((1 - 2 * t) * cubeScaleFactor Q) ^ d

theorem HCPolySupport.cubeVolume_pos {d : ℕ} (Q : TriadicCube d) :

0 < cubeVolume Q

theorem HCPolySupport.cubeVolume_nonneg {d : ℕ} (Q : TriadicCube d) :

0 ≤ cubeVolume Q

theorem HCPolySupport.volume_cubeSet_lt_top {d : ℕ} (Q : TriadicCube d) :

MeasureTheory.volume (cubeSet Q) < ⊤

theorem HCPolySupport.volume_openCubeSet_lt_top {d : ℕ} (Q : TriadicCube d) :

MeasureTheory.volume (openCubeSet Q) < ⊤

theorem HCPolySupport.volume_openCubeSet_eq_volume_cubeSet {d : ℕ} (Q : TriadicCube d) :

MeasureTheory.volume (openCubeSet Q) = MeasureTheory.volume (cubeSet Q)

theorem HCPolySupport.volume_cubeBoundaryLayer_toReal_of_nonneg_le_half {d : ℕ} (Q : TriadicCube d) {t : ℝ} (ht_nonneg : 0 ≤ t) (ht_half : t ≤ 1 / 2) :

(MeasureTheory.volume (cubeBoundaryLayer Q t)).toReal = cubeVolume Q - ((1 - 2 * t) * cubeScaleFactor Q) ^ d

theorem HCPolySupport.integrableOn_cubeSet_iff_integrableOn_openCubeSet {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] {Q : TriadicCube d} {f : Vec d → E} :

MeasureTheory.IntegrableOn f (cubeSet Q) MeasureTheory.volume ↔ MeasureTheory.IntegrableOn f (openCubeSet Q) MeasureTheory.volume

theorem HCPolySupport.setIntegral_cubeSet_eq_setIntegral_openCubeSet {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {Q : TriadicCube d} {f : Vec d → E} :

∫ (x : Vec d) in cubeSet Q, f x = ∫ (x : Vec d) in openCubeSet Q, f x

theorem HCPolySupport.volume_cubeBoundary_eq_zero {d : ℕ} (Q : TriadicCube d) :

MeasureTheory.volume (cubeBoundary Q) = 0

theorem HCPolySupport.volume_cubeBoundaryLayer_zero {d : ℕ} (Q : TriadicCube d) :

MeasureTheory.volume (cubeBoundaryLayer Q 0) = 0