High-contrast homogenization: Entry.Geometry.StandardCell

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

Standard aligned cubes

The centered triadic cube □_j = (-3^j/2, 3^j/2)^d and the standard aligned cubes z + □_k with z = 3^k w, w ∈ ℤ^d, of the paper, built on the TriadicCube descriptors of CoarseGraining. This file holds the cube API that l.source.whitney needs: membership, volume, nesting-or-disjointness of aligned cubes, parents, and the null set of grid faces.

Definitions

Membership

theorem HCPolySupport.HighContrast.Geometry.centeredCube_eq_standardCell {d : ℕ} (j : ℤ) : centeredCube d j = standardCell d j 0

theorem HCPolySupport.HighContrast.Geometry.standardCell_eq_pi_Ioo {d : ℕ} (k : ℤ) (w : Fin d → ℤ) : standardCell d k w = Set.univ.pi fun (i : Fin d) => Set.Ioo ((↑(w i) - 1 / 2) * 3 ^ k) ((↑(w i) + 1 / 2) * 3 ^ k)

theorem HCPolySupport.HighContrast.Geometry.measurableSet_standardCell {d : ℕ} (k : ℤ) (w : Fin d → ℤ) : MeasurableSet (standardCell d k w)

theorem HCPolySupport.HighContrast.Geometry.isOpen_standardCell {d : ℕ} (k : ℤ) (w : Fin d → ℤ) : IsOpen (standardCell d k w)

Volume

theorem HCPolySupport.HighContrast.Geometry.volume_standardCell {d : ℕ} (k : ℤ) (w : Fin d → ℤ) : MeasureTheory.volume (standardCell d k w) = ENNReal.ofReal (3 ^ k) ^ d

theorem HCPolySupport.HighContrast.Geometry.volume_centeredCube {d : ℕ} (j : ℤ) : MeasureTheory.volume (centeredCube d j) = ENNReal.ofReal (3 ^ j) ^ d

theorem HCPolySupport.HighContrast.Geometry.volume_standardCell_pos {d : ℕ} (k : ℤ) (w : Fin d → ℤ) : 0 < MeasureTheory.volume (standardCell d k w)

Nesting and disjointness of aligned cubes

theorem HCPolySupport.HighContrast.Geometry.triadic_interval_subset_of_mem {a : ℝ} (ha : 0 < a) (n : ℕ) {w w' : ℤ} {x : ℝ} (h1 : (↑w - 1 / 2) * a < x) (h2 : x < (↑w + 1 / 2) * a) (h3 : (↑w' - 1 / 2) * (3 ^ n * a) < x) (h4 : x < (↑w' + 1 / 2) * (3 ^ n * a)) : (↑w' - 1 / 2) * (3 ^ n * a) ≤ (↑w - 1 / 2) * a ∧ (↑w + 1 / 2) * a ≤ (↑w' + 1 / 2) * (3 ^ n * a)

One-dimensional core of "aligned triadic cubes are nested or disjoint": if the open intervals ((w - 1/2) a, (w + 1/2) a) and ((w' - 1/2) 3^n a, (w' + 1/2) 3^n a) share a point, the first lies inside the second. Uses only that 3^n is odd.

theorem HCPolySupport.HighContrast.Geometry.standardCell_subset_or_disjoint {d : ℕ} {k k' : ℤ} (hkk' : k ≤ k') (w w' : Fin d → ℤ) : standardCell d k w ⊆ standardCell d k' w' ∨ Disjoint (standardCell d k w) (standardCell d k' w')

Aligned triadic cubes of generations k ≤ k' are nested or disjoint.

theorem HCPolySupport.HighContrast.Geometry.standardCell_disjoint_of_ne {d : ℕ} (k : ℤ) {w w' : Fin d → ℤ} (hww' : w ≠ w') : Disjoint (standardCell d k w) (standardCell d k w')

Distinct aligned cubes of the same generation are disjoint.

theorem HCPolySupport.HighContrast.Geometry.standardCell_subset_of_mem {d : ℕ} {k k' : ℤ} (hkk' : k ≤ k') {w w' : Fin d → ℤ} {x : Vec d} (hx : x ∈ standardCell d k w) (hx' : x ∈ standardCell d k' w') : standardCell d k w ⊆ standardCell d k' w'

A cube of generation k is contained in a cube of generation k' ≥ k that meets it.

theorem HCPolySupport.HighContrast.Geometry.eq_of_standardCell_eq {d : ℕ} [NeZero d] {k k' : ℤ} {w w' : Fin d → ℤ} (h : standardCell d k w = standardCell d k' w') : k = k' ∧ w = w'

The generation and index of an aligned cube are determined by the cube (for d ≥ 1).

Size

theorem HCPolySupport.HighContrast.Geometry.sum_sq_sub_le_of_mem_standardCell {d : ℕ} {k : ℤ} {w : Fin d → ℤ} {x x' : Vec d} (hx : x ∈ standardCell d k w) (hx' : x' ∈ standardCell d k w) : ∑ i : Fin d, (x i - x' i) ^ 2 ≤ ↑d * (3 ^ k) ^ 2

Two points of an aligned cube of generation k are at squared Euclidean distance at most d 3^{2k}.

theorem HCPolySupport.HighContrast.Geometry.standardCell_subset_ball {d : ℕ} {k : ℤ} {w : Fin d → ℤ} {x : Vec d} (hx : x ∈ standardCell d k w) : standardCell d k w ⊆ Metric.ball x (3 ^ k)

An aligned cube of generation k lies in the sup-metric ball of radius 3^k about any of its points.

Grid faces

def HCPolySupport.HighContrast.Geometry.gridFaces (d : ℕ) (k : ℤ) : Set (Vec d)

The faces of the generation-k grid: the hyperplanes x_i = (n + 1/2) 3^k.

Equations

• HCPolySupport.HighContrast.Geometry.gridFaces d k = ⋃ (i : Fin d), ⋃ (n : ℤ), {x : HCPolySupport.Vec d | x i = (↑n + 1 / 2) * 3 ^ k}

theorem HCPolySupport.HighContrast.Geometry.volume_gridFaces {d : ℕ} (k : ℤ) : MeasureTheory.volume (gridFaces d k) = 0

theorem HCPolySupport.HighContrast.Geometry.exists_mem_standardCell_of_not_mem_gridFaces {d : ℕ} {k : ℤ} {x : Vec d} (hx : x ∉ gridFaces d k) : ∃ (w : Fin d → ℤ), x ∈ standardCell d k w

A point off the generation-k grid faces lies in an aligned cube of generation k.