High-contrast homogenization: #
Provider.PolynomialHomogenization.Root.RowSupply.GeneralAdaptedCellFillingDescendants
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Common-parent descendants for a general adapted filling #
Once an arbitrary adapted target is enclosed in one cell of the filling grid,
every selected filling cell corresponds to a descendant of the associated
reference origin cube. This is the geometric bridge from the general filling
to maxDescendantNormalizedBlockResponseAtScale.
theorem
HCPolySupport.HighContrast.RowSupply.translateCube_mem_descendantsAtScale_originCube_of_mem_adaptedTarget_filling
{d : ℕ}
{p q : Mat d}
(hq : Matrix.PosDef q)
{n j M : ℤ}
(hnM : n ≤ M)
{y : Vec d}
{Z : ℤ → Finset (Fin d → ℤ)}
(hZ : ∀ (r : ℤ), ↑(Z r) = Transport.fillingIndex q n (adaptedCellTranslate p j y) r)
(hEnclose : adaptedCellTranslate p j y ⊆ adaptedCell q M)
{r : ℤ}
{w : Fin d → ℤ}
(hw : w ∈ Z r)
:
A cell selected by a general q-grid filling of a p-adapted target is a
reference descendant of any enclosing q-grid parent above the filling's
starting scale.