High-contrast homogenization: Provider.Regularity.TranslatedCubeGeometry

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

Triadic cubes displaced by a fixed vector

A triadic cube displaced by a fixed vector is again a half-open box of the same side length. Two facts about such a displacement are recorded here.

• The set where the displaced cube and the undisplaced cube disagree has volume at most twice the dimension times the relative displacement times the cube volume: a fixed displacement is asymptotically invisible on a growing cube.
• A displaced cube is compatible with the triadic grid at every scale whose side length divides each coordinate of the displacement, so a triadic cube of that scale is either contained in the displaced cube or disjoint from it.

Both statements are elementary interval arithmetic, and both are used to bound the positive Besov norm of the difference of two cube indicator functions.

def HCPolySupport.HighContrast.translatedCubeSet {d : ℕ} (Q : TriadicCube d) (t : Vec d) : Set (Vec d)

The half-open realization of a triadic cube displaced by a fixed vector.

Equations

• HCPolySupport.HighContrast.translatedCubeSet Q t = HCPolySupport.translateSet t (HCPolySupport.cubeSet Q)

def HCPolySupport.HighContrast.cubeTranslationGap {d : ℕ} (Q : TriadicCube d) (u v : Vec d) : Set (Vec d)

The set on which two displacements of a triadic cube disagree.

Equations

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

Coordinate description

theorem HCPolySupport.HighContrast.mem_translatedCubeSet_iff {d : ℕ} {Q : TriadicCube d} {t x : Vec d} : x ∈ translatedCubeSet Q t ↔ ∀ (i : Fin d), (↑(Q.index i) - 1 / 2) * cubeScaleFactor Q + t i ≤ x i ∧ x i < (↑(Q.index i) + 1 / 2) * cubeScaleFactor Q + t i

theorem HCPolySupport.HighContrast.translatedCubeSet_eq_pi_Ico {d : ℕ} (Q : TriadicCube d) (t : Vec d) : translatedCubeSet Q t = Set.univ.pi fun (i : Fin d) => Set.Ico ((↑(Q.index i) - 1 / 2) * cubeScaleFactor Q + t i) ((↑(Q.index i) + 1 / 2) * cubeScaleFactor Q + t i)

@[simp]

theorem HCPolySupport.HighContrast.translatedCubeSet_zero {d : ℕ} (Q : TriadicCube d) : translatedCubeSet Q 0 = cubeSet Q

theorem HCPolySupport.HighContrast.measurableSet_translatedCubeSet {d : ℕ} (Q : TriadicCube d) (t : Vec d) : MeasurableSet (translatedCubeSet Q t)

theorem HCPolySupport.HighContrast.measurableSet_cubeTranslationGap {d : ℕ} (Q : TriadicCube d) (u v : Vec d) : MeasurableSet (cubeTranslationGap Q u v)

Volumes

theorem HCPolySupport.HighContrast.volume_translatedCubeSet {d : ℕ} (Q : TriadicCube d) (t : Vec d) : MeasureTheory.volume (translatedCubeSet Q t) = MeasureTheory.volume (cubeSet Q)

theorem HCPolySupport.HighContrast.volume_translatedCubeSet_ne_top {d : ℕ} (Q : TriadicCube d) (t : Vec d) : MeasureTheory.volume (translatedCubeSet Q t) ≠ ⊤

theorem HCPolySupport.HighContrast.volume_translatedCubeSet_toReal {d : ℕ} (Q : TriadicCube d) (t : Vec d) : (MeasureTheory.volume (translatedCubeSet Q t)).toReal = cubeVolume Q

The part common to two displacements

theorem HCPolySupport.HighContrast.volume_inter_translatedCubeSet_toReal {d : ℕ} (Q : TriadicCube d) (u v : Vec d) (huv : ∀ (i : Fin d), |u i - v i| ≤ cubeScaleFactor Q) : (MeasureTheory.volume (translatedCubeSet Q u ∩ translatedCubeSet Q v)).toReal = ∏ i : Fin d, (cubeScaleFactor Q - |u i - v i|)

The volume common to two displacements of a triadic cube is the product of the shortened side lengths.

The relative volume of the disagreement set

theorem HCPolySupport.HighContrast.volume_cubeTranslationGap_toReal_le {d : ℕ} (Q : TriadicCube d) (u v : Vec d) {V : ℝ} (hV : 0 ≤ V) (hVle : V ≤ cubeScaleFactor Q) (huv : ∀ (i : Fin d), |u i - v i| ≤ V) : (MeasureTheory.volume (cubeTranslationGap Q u v)).toReal ≤ 2 * ↑d * (V / cubeScaleFactor Q) * cubeVolume Q

Two displacements differing by at most V in every coordinate disagree only on a set whose relative volume is at most twice the dimension times the relative difference.

Compatibility with the triadic grid

theorem HCPolySupport.HighContrast.cubeSet_subset_or_disjoint_translatedCubeSet {d : ℕ} {R A : TriadicCube d} {t : Vec d} (hscale : R.scale ≤ A.scale) (hlat : ∀ (i : Fin d), ∃ (p : ℤ), t i = ↑p * cubeScaleFactor R) : cubeSet R ⊆ translatedCubeSet A t ∨ Disjoint (cubeSet R) (translatedCubeSet A t)

A triadic cube whose side length divides every coordinate of the displacement is either contained in the displaced cube or disjoint from it.