High-contrast homogenization: Provider.Response.NestedAlignedGeometry #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Nested aligned-cell geometry #
Aligned cells subdivide in two stages by the mixed-radix label obtained from a parent label and a centred residual label. This gives both containment of the nested label in the terminal index and an exact reindexing of normalized cell averages.
theorem
HCPolySupport.HighContrast.Response.nestedLabel_mem_alignedIndex
{d : ℕ}
{q : Mat d}
(hq : Matrix.PosDef q)
{k s t : ℤ}
(hks : k ≤ s)
(hst : s ≤ t)
{w z : Fin d → ℤ}
(hw : w ∈ alignedIndex q k s)
(hz : z ∈ alignedIndex q s t)
:
A two-stage aligned label remains aligned with the terminal cell.
theorem
HCPolySupport.HighContrast.Response.avsum_nestedLabel_alignedIndex
{d : ℕ}
{q : Mat d}
(hq : Matrix.PosDef q)
{k s t : ℤ}
(hks : k ≤ s)
(hst : s ≤ t)
(f : (Fin d → ℤ) → ℝ)
:
(avsum (alignedIndex q k s) fun (w : Fin d → ℤ) =>
avsum (alignedIndex q s t) fun (z : Fin d → ℤ) => f (nestedLabel k s z w)) = avsum (alignedIndex q k t) f
Two-stage normalized aligned-cell averaging is exact.