High-contrast homogenization: Provider.Quenched.UnitRangeSubadditivity

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

Subadditivity over the standard aligned cubes

The renormalization argument compares the coarse block of a cell with the average of the coarse blocks of the cells of an inner generation that subdivide it. The prior subadditivity theorem is stated at the cell centred at the origin and in the adapted dialect; this file reads it in the standard dialect, at the identity grid, and translates it to an arbitrary aligned parent.

The translation is the sample-level covariance of the coarse block: a translated cell reads the translated sample. The inner cells of the translated parent are the inner cells of the origin parent with their indices shifted by the parent's index, scaled by the ratio of the two generations, so the index set of the average is the one already counted by card_centredIndexFinset.

The origin parent, in the standard dialect

theorem HCPolySupport.HighContrast.Quenched.toFullBlockMat_coarseBlock_centeredCube_le_average {d : ℕ} [NeZero d] {l k : ℤ} (hlk : l ≤ k) (a : CoeffSpace d) : toFullBlockMat (coarseBlock (centeredCube d k) a) ≤ (↑(centredIndexFinset d l k).card)⁻¹ • ∑ t ∈ centredIndexFinset d l k, toFullBlockMat (coarseBlock (standardCell d l t) a)

Subadditivity at the centred parent. The coarse block of □_k is below the average of the coarse blocks of the scale-l standard cubes centred in it.

The translation to an aligned parent

def HCPolySupport.HighContrast.Quenched.innerShift {d : ℕ} (k l : ℤ) (w t : Fin d → ℤ) : Fin d → ℤ

The index shift carrying the inner cells of the centred parent to the inner cells of the aligned parent.

Equations

• HCPolySupport.HighContrast.Quenched.innerShift k l w t i = t i + w i * 3 ^ (k - l).toNat

def HCPolySupport.HighContrast.Quenched.parentShift {d : ℕ} (k : ℤ) (w : Fin d → ℤ) : Fin d → ℤ

The translation vector of an aligned parent.

Equations

• HCPolySupport.HighContrast.Quenched.parentShift k w i = w i * 3 ^ k.toNat

theorem HCPolySupport.HighContrast.Quenched.toFullBlockMat_coarseBlock_standardCell_le_average {d : ℕ} [NeZero d] {l k : ℤ} (hl : 0 ≤ l) (hlk : l ≤ k) (w : Fin d → ℤ) (a : CoeffSpace d) : toFullBlockMat (coarseBlock (standardCell d k w) a) ≤ (↑(centredIndexFinset d l k).card)⁻¹ • ∑ t ∈ centredIndexFinset d l k, toFullBlockMat (coarseBlock (standardCell d l (innerShift k l w t)) a)

Subadditivity at an aligned parent. The coarse block of a standard aligned cube is below the average of the coarse blocks of the scale-l standard cubes that subdivide it.