High-contrast homogenization: Entry.Geometry.SourceWhitneyDecomposition #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Source Whitney Decomposition #
For W = y + ⋄_j^q with |q⁻¹| ≤ 2, the maximal standard aligned cubes of generation at
most j contained in W are pairwise disjoint subsets of W that cover W up to a
Lebesgue-null set, each generation carries only finitely many of them, and the row of
generation r ≤ j obeys the relative-volume bound
Σ_{z ∈ 𝒵_r(W)} |□_r| / |W| ≤ 12 d^{3/2} 3^{r-j}. This is the source Whitney
decomposition l.source.whitney, used to estimate the source term.
The maximal cubes exhaust W #
The remaining measure-theoretic half of l.source.whitney: for
W = y + q □_j with q invertible, the maximal standard aligned cubes of generation at
most j contained in W cover W up to a Lebesgue-null set.
The null set is the union ⋃ k : ℤ, gridFaces d k of all grid faces of all generations,
which is null because ℤ is countable. Off that set, every x ∈ W lies in a standard
aligned cube of every generation, and cubes of very negative generation are small enough to
fit inside W (which is open); a maximal cube through x then exists.
The maximal cubes exhaust W up to a null set. For W = y + q □_j with q
invertible, the maximal standard aligned cubes of generation ≤ j inside W cover W
up to a Lebesgue-null set.
Standard cubes inside an adapted cube #
l.source.whitney. For W = y + ⋄_j^q, the
maximal standard aligned cubes contained in W with generation at most j partition W
up to a null set (SourceWhitneyDecomposition.lean and MaximalCells.lean), and for r ≤ j
those of
generation r satisfy
Σ_{z ∈ 𝒵_r(W)} |□_r| / |W| ≤ 12 d^{3/2} 3^{r-j}.
This file proves the volume bound and states the lemma as one package, source_whitney.
The manuscript sets q = 𝒬(m) and uses only |q⁻¹| ≤ 2 from e.rounded.grid.bounds
(near e.rounded.grid.bounds). Here that bound is the hypothesis InverseNormLE q 2; the constant
12 d^{3/2} = 4d · √d · 3 is produced by the proof, uniformly in q.
The row of generation r against the target #
A row of maximal cubes never exceeds the target: its members are disjoint subsets
of W.
Every point of a maximal cube of generation r < j is within Euclidean distance
√d 3^{r+1} of a point outside W: the parent escapes W.
The row bound in measure form. For r < j and |q⁻¹| ≤ K, the maximal cubes of
generation r have total volume at most 2d · K √d 3^{r+1} · 3^{-j} times |W|.
Finite sums over the row #
The volumes of finitely many maximal cubes of one generation add up to the volume of their union, which lies inside the union of the whole row.
The row of generation r is finite: its cubes are disjoint, of equal positive volume,
and lie in a set of finite volume.
Conversion of a measure-form row bound |⋃ row| ≤ C |W| into the printed relative-volume
form Σ |□_r| / |W| ≤ C.
The printed constant #
l.source.whitney, the volume bound #
e.source.whitney.volumes. Let W = y + ⋄_j^q with |q⁻¹| ≤ 2, and r ≤ j.
Then the maximal standard aligned cubes of generation r inside W (among those of
generation at most j) satisfy Σ_{z ∈ 𝒵_r(W)} |□_r| / |W| ≤ 12 d^{3/2} 3^{r-j}.
l.source.whitney, the full statement #
l.source.whitney (Standard cubes inside an adapted cube). Let W = y + ⋄_j^q with
|q⁻¹| ≤ 2 (the bound e.rounded.grid.bounds satisfied by q = 𝒬(m)), y ∈ ℝ^d, j ∈ ℤ.
The maximal standard aligned cubes contained in W with generations at most j are
pairwise disjoint subsets of W covering W up to a null set, each generation r has
finitely many of them, and Σ_{z ∈ 𝒵_r(W)} |□_r| / |W| ≤ 12 d^{3/2} 3^{r-j} for r ≤ j.