High-contrast homogenization: Provider.Transport.WhitneyLayer

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

The boundary layer of a target cell

The maximal filling of l.two.grid.whitney selects a cell of one grid inside a cell of another exactly when the selected cell fits and its parent does not. Every cell it selects, and every point it fails to cover, therefore lies in a thin layer along the boundary of the target: the escaping ancestor joins a point of the target to a point outside it, and the whole ancestor has diameter comparable to its own side length.

This file proves the measure of that layer, the boundary-layer volume of an adapted cube, in the form the row and residual bounds of e.source.whitney.volumes consume. In the coordinates of the target the layer is the union of the 2d coordinate slabs along the faces of a centered triadic cube, and each slab has relative volume at most twice the layer width over the side length. The escaping ancestor contributes its own side length through the cross-grid factor |p^{-1}q|: a displacement inside an ancestor of the second grid has length at most √d 3^c there, and the linear change of coordinates to the first grid multiplies lengths by at most the operator norm of p^{-1}q.

The operator norm controls a coordinate of a displacement

theorem HCPolySupport.HighContrast.Transport.abs_matVecMul_le_of_abs_le {d : ℕ} (M : Mat d) {z : Vec d} {c : ℝ} (hz : ∀ (k : Fin d), |z k| ≤ c) (i : Fin d) : |matVecMul M z i| ≤ ‖M‖ * (√↑d * c)

A coordinate of a linear image is controlled by the operator norm. If every coordinate of z is at most c in modulus, then every coordinate of M z is at most ‖M‖ √d c.

The slab along one pair of faces of a centered cube

theorem HCPolySupport.HighContrast.Transport.volume_centeredCube_eq_prod {d : ℕ} (j : ℤ) : MeasureTheory.volume (centeredCube d j) = ∏ _i : Fin d, ENNReal.ofReal (3 ^ j)

The volume of a centered triadic cube as the product of its side lengths.

theorem HCPolySupport.HighContrast.Transport.volume_layer_centeredCube_le {d : ℕ} (j : ℤ) {t : ℝ} (ht : 0 ≤ t) : MeasureTheory.volume {z : Vec d | z ∈ centeredCube d j ∧ ∃ (i : Fin d), 1 / 2 * 3 ^ j - t ≤ |z i|} ≤ ENNReal.ofReal (2 * ↑d * t * 3 ^ (-j)) * MeasureTheory.volume (centeredCube d j)

The boundary layer of a centered triadic cube. The points of □_j within t of one of the 2d faces have relative volume at most 2 d t 3^{-j}; this is the boundary-layer volume bound in the coordinates of the cube.

The layer of a target cell of a second grid

theorem HCPolySupport.HighContrast.Transport.adaptedCellTranslate_eq_image {d : ℕ} (p : Mat d) (j : ℤ) (y : Vec d) : adaptedCellTranslate p j y = (fun (z : Vec d) => y + matVecMul p z) '' centeredCube d j

A translated adapted cell is the affine image of the centered cube.

theorem HCPolySupport.HighContrast.Transport.volume_image_affine {d : ℕ} (p : Mat d) (y : Vec d) (S : Set (Vec d)) : MeasureTheory.volume ((fun (z : Vec d) => y + matVecMul p z) '' S) = ENNReal.ofReal |Matrix.det p| * MeasureTheory.volume S

An affine image scales volume by the modulus of the determinant.

theorem HCPolySupport.HighContrast.Transport.volume_le_of_escaping_ancestor {d : ℕ} {p q : Mat d} (hp : Matrix.PosDef p) {j c : ℤ} {y : Vec d} {A : Set (Vec d)} (hAW : A ⊆ adaptedCellTranslate p j y) (hesc : ∀ x ∈ A, ∃ (v : Fin d → ℤ), x ∈ adaptedCellAt q c v ∧ ¬adaptedCellAt q c v ⊆ adaptedCellTranslate p j y) : MeasureTheory.volume A ≤ ENNReal.ofReal (2 * ↑d * √↑d * ‖p⁻¹ * q‖ * 3 ^ (c - j)) * MeasureTheory.volume (adaptedCellTranslate p j y)

The cells that escape the target lie in its boundary layer. If every point of A lies in the target cell y + ⋄_j^p and also in some aligned q-cell of scale c that is not contained in the target, then A has relative volume at most 2 d^{3/2} |p^{-1}q| 3^{c-j}.

This is the boundary-layer volume of an adapted cube in the form the row and residual bounds of e.source.whitney.volumes consume: for a selected cell of scale a < n the escaping ancestor is its own parent, c = a + 1, and for a point left uncovered at the cutoff J it is the cell of scale c = J that contains it.