High-contrast homogenization: Provider.Recurrence.AdaptedSubadditivity

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

The coarse block is subadditive over the aligned subdivision

This is the subadditivity among the coarse-block properties taken from HC, in the form the fixed-grid recurrence consumes it at its averaging step: for a rounded grid q, scales j ≤ p, and the aligned subdivision of ⋄_p^q into its 3^{d(p-j)} scale-j children, 𝐀(⋄_p^q) ≤ 3^{-d(p-j)} Σ_w 𝐀(z_w + ⋄_j^q), which is the first display of e.fixed.geometry.parent.child with the uniform weights |U_i| / |U| of a subdivision into cells of equal volume.

Nothing here is specific to the grid beyond the geometry already recorded: the children are nonempty bounded open convex domains contained in the parent, pairwise disjoint, and covering the parent up to a null set, which is exactly the hypothesis of the general subadditivity of the companion file; and they are translates of one another, so their common volume collapses the printed weight |U_i| / |U| to 3^{-d(p-j)}. A field of the coefficient space enters through a measurable everywhere elliptic representative, which changes no coarse block.

The conclusion is recorded twice: as the quadratic-form inequality that defines the Loewner order on doubled blocks, and as the Loewner inequality itself between the flattened matrices, where the average on the right is the honest matrix average of the printed display.

The size of the aligned subdivision

theorem HCPolySupport.HighContrast.Recurrence.card_alignedIndex {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) {j p : ℤ} (hjp : j ≤ p) {Z : Finset (Fin d → ℤ)} (hZ : ↑Z = {w : Fin d → ℤ | adaptedCellCenter q j w ∈ adaptedCell q p}) : Z.card = 3 ^ (d * (p - j).toNat)

The index set of the aligned subdivision has 3^{d(p-j)} elements, so it is nonempty.

The printed display, as a quadratic-form inequality

theorem HCPolySupport.HighContrast.Recurrence.coarseBlock_adaptedCell_le_average {d : ℕ} [NeZero d] {q : Mat d} (hq : Matrix.PosDef q) {j p : ℤ} (hjp : j ≤ p) {Z : Finset (Fin d → ℤ)} (hZ : ↑Z = {w : Fin d → ℤ | adaptedCellCenter q j w ∈ adaptedCell q p}) (a : CoeffSpace d) (X : BlockVec d) : 1 / 2 * blockVecDot X (blockMatVecMul (coarseBlock (adaptedCell q p) a) X) ≤ (↑Z.card)⁻¹ * ∑ w ∈ Z, 1 / 2 * blockVecDot X (blockMatVecMul (coarseBlock (adaptedCellAt q j w) a) X)

Subadditivity of the coarse block over the aligned subdivision. This is e.fixed.geometry.parent.child at the aligned subdivision of the adapted cubes, in the quadratic form that defines the Loewner order on doubled blocks.

The printed display, as a Loewner inequality of matrices

theorem HCPolySupport.HighContrast.Recurrence.toFullBlockMat_coarseBlock_adaptedCell_le_average {d : ℕ} [NeZero d] {q : Mat d} (hq : Matrix.PosDef q) {j p : ℤ} (hjp : j ≤ p) {Z : Finset (Fin d → ℤ)} (hZ : ↑Z = {w : Fin d → ℤ | adaptedCellCenter q j w ∈ adaptedCell q p}) (a : CoeffSpace d) : toFullBlockMat (coarseBlock (adaptedCell q p) a) ≤ (↑Z.card)⁻¹ • ∑ w ∈ Z, toFullBlockMat (coarseBlock (adaptedCellAt q j w) a)

𝐀(⋄_p^q) ≤ 3^{-d(p-j)} Σ_w 𝐀(z_w + ⋄_j^q). The first display of e.fixed.geometry.parent.child over the aligned subdivision, in the Loewner order of the flattened doubled blocks.

The positivity and subadditivity clauses together