High-contrast homogenization:

Provider.PolynomialHomogenization.Root.RowSupply.DescendantHomogenizationErrorInfinityTwo

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

Descendant control for the quadratic homogenization error

The all-depth response row on a cube also controls the corresponding row on any descendant. Reindexing the geometric weights records the exact triadic scale loss.

theorem HCPolySupport.HighContrast.RowSupply.homogenizationErrorOnCube_infinity_two_le_of_mem_descendantsAtScale {d : ℕ} [NeZero d] {Q R : TriadicCube d} {k : ℤ} (a : Book.Ch02.TriadicCoeffFamily d) (a0 : Mat d) {s : ℝ} (hs : 0 < s) (hR : R ∈ descendantsAtScale Q k) : Book.Ch02.HomogenizationErrorOnCube R s Book.Ch02.MultiscaleExponent.infinity (Book.Ch02.MultiscaleExponent.finite 2) a a0 ≤ Real.rpow 3 (s * ↑(Q.scale - k).toNat) * Book.Ch02.HomogenizationErrorOnCube Q s Book.Ch02.MultiscaleExponent.infinity (Book.Ch02.MultiscaleExponent.finite 2) a a0

A descendant at depth h has quadratic homogenization error at most 3^(s h) times that of its parent.