High-contrast homogenization: Provider.Recurrence.AdaptedCellDomain

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

The adapted cell as a bounded open convex domain

The coarse-response formalism taken from HC is developed over bounded open convex domains: the variational identity that reads the coarse block off the response functional, the restriction of an a-harmonic competitor, and the upper bound that makes the response functional a genuine supremum all take that hypothesis. The adapted cubes of a rounded geometry are linear images of triadic cubes under an invertible grid map, so they are bounded open convex domains as well, and this file records that.

An invertible grid map is an open map because its image is the preimage under the inverse map, which is continuous; it preserves boundedness because a linear map moves the coordinate bound by the sum of the absolute entries; and it preserves convexity because it is linear. Cubes are nonempty because they contain their centers, and a nonempty open set has positive volume, so the volume normalizations of the response functional are legitimate on every adapted cell. Finally, the aligned cells at one scale are translates of each other, so they all have the same volume — the fact that turns the weights |U_i| / |U| of e.fixed.geometry.parent.child into the uniform weights 3^{-d(p-j)} of the recurrence.

Linear images under an invertible grid map

theorem HCPolySupport.HighContrast.Recurrence.image_matVecMul_eq_preimage_inv {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) (S : Set (Vec d)) : matVecMul q '' S = matVecMul q⁻¹ ⁻¹' S

The image of a set under an invertible grid map is the preimage under the inverse map.

theorem HCPolySupport.HighContrast.Recurrence.isOpen_image_matVecMul {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) {S : Set (Vec d)} (hS : IsOpen S) : IsOpen (matVecMul q '' S)

An invertible grid map is an open map.

theorem HCPolySupport.HighContrast.Recurrence.isBoundedDomain_image_matVecMul {d : ℕ} (M : Mat d) {S : Set (Vec d)} (hS : IsBoundedDomain S) : IsBoundedDomain (matVecMul M '' S)

A linear map moves a coordinate bound by the sum of the absolute entries.

theorem HCPolySupport.HighContrast.Recurrence.isOpenBoundedConvexDomain_image_matVecMul {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) {S : Set (Vec d)} (hS : IsOpenBoundedConvexDomain S) : IsOpenBoundedConvexDomain (matVecMul q '' S)

The invertible linear image of a bounded open convex domain is one.

Cubes contain their centers

theorem HCPolySupport.HighContrast.Recurrence.standardCellCenter_mem_standardCell {d : ℕ} (k : ℤ) (w : Fin d → ℤ) : standardCellCenter k w ∈ standardCell d k w

A standard aligned cube contains its center.

theorem HCPolySupport.HighContrast.Recurrence.standardCell_nonempty {d : ℕ} (k : ℤ) (w : Fin d → ℤ) : (standardCell d k w).Nonempty

A standard aligned cube is nonempty.

theorem HCPolySupport.HighContrast.Recurrence.centeredCube_nonempty {d : ℕ} (k : ℤ) : (centeredCube d k).Nonempty

A centered triadic cube is nonempty.

The adapted cells are domains

theorem HCPolySupport.HighContrast.Recurrence.isOpenBoundedConvexDomain_adaptedCell {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) (k : ℤ) : IsOpenBoundedConvexDomain (adaptedCell q k)

The adapted cell ⋄_k^q is a bounded open convex domain.

theorem HCPolySupport.HighContrast.Recurrence.isOpenBoundedConvexDomain_adaptedCellAt {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) (k : ℤ) (w : Fin d → ℤ) : IsOpenBoundedConvexDomain (adaptedCellAt q k w)

An aligned adapted cell is a bounded open convex domain.

theorem HCPolySupport.HighContrast.Recurrence.adaptedCell_nonempty {d : ℕ} (q : Mat d) (k : ℤ) : (adaptedCell q k).Nonempty

An adapted cell is nonempty.

theorem HCPolySupport.HighContrast.Recurrence.adaptedCellAt_nonempty {d : ℕ} (q : Mat d) (k : ℤ) (w : Fin d → ℤ) : (adaptedCellAt q k w).Nonempty

An aligned adapted cell is nonempty.

Volumes of adapted cells

theorem HCPolySupport.HighContrast.Recurrence.volume_adaptedCell_pos {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) (k : ℤ) : 0 < MeasureTheory.volume (adaptedCell q k)

An adapted cell has positive volume.

theorem HCPolySupport.HighContrast.Recurrence.volume_adaptedCellAt_pos {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) (k : ℤ) (w : Fin d → ℤ) : 0 < MeasureTheory.volume (adaptedCellAt q k w)

An aligned adapted cell has positive volume.

theorem HCPolySupport.HighContrast.Recurrence.volume_adaptedCell_lt_top {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) (k : ℤ) : MeasureTheory.volume (adaptedCell q k) < ⊤

An adapted cell has finite volume.

theorem HCPolySupport.HighContrast.Recurrence.toReal_volume_adaptedCell_pos {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) (k : ℤ) : 0 < (MeasureTheory.volume (adaptedCell q k)).toReal

The volume normalization of an adapted cell is a positive real.

theorem HCPolySupport.HighContrast.Recurrence.volume_adaptedCellAt {d : ℕ} (q : Mat d) (k : ℤ) (w : Fin d → ℤ) : MeasureTheory.volume (adaptedCellAt q k w) = MeasureTheory.volume (adaptedCell q k)

The aligned cells at one scale all have the volume of the cell at the origin, being translates of it. This is what turns the weights |U_i| / |U| of e.fixed.geometry.parent.child into uniform weights.