High-contrast homogenization: Provider.Quenched.UnitRangeInnerCells

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

The inner cells of an aligned parent

The renormalization argument averages the coarse blocks of the scale-l cells that subdivide a scale-k cell centred in □_m. Three facts about that family are needed before the concentration estimate and the subadditivity can be combined.

Their centres lie in □_{m+1}, not necessarily in □_m: a parent centred near the boundary of □_m has inner cells centred outside it, so the coarse-ellipticity datum has to be read one generation higher. The average of their coarse blocks is a doubled block in its own right. And the index map of the subdivision is injective, so the family may be indexed by the cells themselves.

The inner cells sit one generation higher

theorem HCPolySupport.HighContrast.Quenched.standardCellCenter_innerShift_mem_centeredCube_succ {d : ℕ} {l k m : ℤ} (hlk : l ≤ k) (hkm : k ≤ m) {w t : Fin d → ℤ} (hw : standardCellCenter k w ∈ centeredCube d m) (ht : standardCellCenter l t ∈ centeredCube d k) : standardCellCenter l (innerShift k l w t) ∈ centeredCube d (m + 1)

The inner cells of a parent centred in □_m are centred in □_{m+1}. This is why the coarse-ellipticity datum is read at the generation m + 1 in the subdivision step.

The average of a family of doubled blocks

noncomputable def HCPolySupport.HighContrast.Quenched.avgBlockOf {d : ℕ} {ι : Type u_1} (Z : Finset ι) (M : ι → BlockMat d) : BlockMat d

The average of a finite family of doubled blocks.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.HighContrast.Quenched.blockMatEntry_avgBlockOf {d : ℕ} {ι : Type u_1} (Z : Finset ι) (M : ι → BlockMat d) (α β : BlockCoord d) : blockMatEntry (avgBlockOf Z M) α β = (↑Z.card)⁻¹ * ∑ t ∈ Z, blockMatEntry (M t) α β

theorem HCPolySupport.HighContrast.Quenched.toFullBlockMat_avgBlockOf {d : ℕ} {ι : Type u_1} (Z : Finset ι) (M : ι → BlockMat d) : toFullBlockMat (avgBlockOf Z M) = (↑Z.card)⁻¹ • ∑ t ∈ Z, toFullBlockMat (M t)

The subdivision index map

theorem HCPolySupport.HighContrast.Quenched.innerShift_injective {d : ℕ} (k l : ℤ) (w : Fin d → ℤ) : Function.Injective (innerShift k l w)

theorem HCPolySupport.HighContrast.Quenched.card_image_innerShift {d : ℕ} (k l : ℤ) (w : Fin d → ℤ) (Z : Finset (Fin d → ℤ)) : (Finset.image (innerShift k l w) Z).card = Z.card

theorem HCPolySupport.HighContrast.Quenched.avgBlockOf_image_innerShift {d : ℕ} {k l : ℤ} (w : Fin d → ℤ) (Z : Finset (Fin d → ℤ)) (F : (Fin d → ℤ) → BlockMat d) : avgBlockOf (Finset.image (innerShift k l w) Z) F = avgBlockOf Z fun (t : Fin d → ℤ) => F (innerShift k l w t)

Subadditivity in block form

theorem HCPolySupport.HighContrast.Quenched.blockMatLoewnerLE_coarseBlock_avgBlockOf {d : ℕ} [NeZero d] {l k : ℤ} (hl : 0 ≤ l) (hlk : l ≤ k) (w : Fin d → ℤ) (a : CoeffSpace d) : BlockMatLoewnerLE (coarseBlock (standardCell d k w) a) (avgBlockOf (Finset.image (innerShift k l w) (centredIndexFinset d l k)) fun (u : Fin d → ℤ) => coarseBlock (standardCell d l u) a)

Subadditivity against the average of the inner cells, in the Loewner order of doubled blocks and indexed by the inner cells themselves.