High-contrast homogenization: Annealed.WitnessBlock

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

The coarse response of the constant identity field is uniformly dominated

The reference block of e.coarse.ellipticity has to dominate the coarse response 𝐀(z + □_k; a) of every standard aligned cube, at every scale. For the constant identity field the domination is scale and location uniform, and it is obtained from a single admissible competitor: the constant state. Its averaged energy is the doubled square norm of the prescribed boundary data, independently of the cube; combined with the nonnegativity of the variational quantity this bounds every entry of the coarse response by an absolute constant, hence its quadratic form by a multiple of the doubled identity.

Consequently no discount factor is needed: the domination holds at the exponent g = 0 of Set.Ico 0 1, at which 3^{g(m-k)} is one.

The doubled square norm and the doubled identity

def HCPolySupport.HighContrast.blockNormSq {d : ℕ} (X : BlockVec d) : ℝ

The square norm of a doubled vector.

Equations

• HCPolySupport.HighContrast.blockNormSq X = HCPolySupport.vecNormSq X.1 + HCPolySupport.vecNormSq X.2

theorem HCPolySupport.HighContrast.blockNormSq_nonneg {d : ℕ} (X : BlockVec d) : 0 ≤ blockNormSq X

theorem HCPolySupport.HighContrast.vecNormSq_pos {d : ℕ} {x : Vec d} (hx : x ≠ 0) : 0 < vecNormSq x

theorem HCPolySupport.HighContrast.blockNormSq_pos {d : ℕ} {X : BlockVec d} (hX : X ≠ 0) : 0 < blockNormSq X

theorem HCPolySupport.HighContrast.vecNormSq_single' {d : ℕ} (i : Fin d) : vecNormSq (Pi.single i 1) = 1

theorem HCPolySupport.HighContrast.vecNormSq_zero' {d : ℕ} : vecNormSq 0 = 0

theorem HCPolySupport.HighContrast.blockNormSq_blockBasis {d : ℕ} (γ : BlockCoord d) : blockNormSq (blockBasis γ) = 1

theorem HCPolySupport.HighContrast.vecNormSq_add_le {d : ℕ} (x y : Vec d) : vecNormSq (x + y) ≤ 2 * (vecNormSq x + vecNormSq y)

theorem HCPolySupport.HighContrast.blockNormSq_add_le {d : ℕ} (X Y : BlockVec d) : blockNormSq (X + Y) ≤ 2 * (blockNormSq X + blockNormSq Y)

theorem HCPolySupport.HighContrast.sum_sq_toFullBlockVec {d : ℕ} (X : BlockVec d) : ∑ α : BlockCoord d, toFullBlockVec X α ^ 2 = blockNormSq X

theorem HCPolySupport.HighContrast.card_blockCoord {d : ℕ} : Fintype.card (BlockCoord d) = 2 * d

def HCPolySupport.HighContrast.scaledBlockIdentity (d : ℕ) (c : ℝ) : BlockMat d

A scalar multiple of the doubled identity.

Equations

• HCPolySupport.HighContrast.scaledBlockIdentity d c = { upperLeft := c • 1, upperRight := 0, lowerLeft := 0, lowerRight := c • 1 }

theorem HCPolySupport.HighContrast.matVecMul_smul_identity {d : ℕ} (c : ℝ) (x : Vec d) : matVecMul (c • 1) x = fun (i : Fin d) => c * x i

theorem HCPolySupport.HighContrast.matVecMul_zero_left {d : ℕ} (x : Vec d) : matVecMul 0 x = 0

theorem HCPolySupport.HighContrast.blockVecDot_scaledBlockIdentity {d : ℕ} (c : ℝ) (X : BlockVec d) : blockVecDot X (blockMatVecMul (scaledBlockIdentity d c) X) = c * blockNormSq X

theorem HCPolySupport.HighContrast.isSymmetricBlockMat_scaledBlockIdentity {d : ℕ} (c : ℝ) : IsSymmetricBlockMat (scaledBlockIdentity d c)

theorem HCPolySupport.HighContrast.blockPosDef_scaledBlockIdentity {d : ℕ} {c : ℝ} (hc : 0 < c) : Book.Ch02.BlockPosDef (scaledBlockIdentity d c)

theorem HCPolySupport.HighContrast.blockMatrixOfCoeff_identity {d : ℕ} : blockMatrixOfCoeff 1 = scaledBlockIdentity d 1

The constant competitor

def HCPolySupport.HighContrast.constBlockState {d : ℕ} (P : BlockVec d) : BlockState d

The constant admissible state with prescribed doubled boundary data.

Equations

• HCPolySupport.HighContrast.constBlockState P = { potential := fun (x : HCPolySupport.Vec d) => P.1, flux := fun (x : HCPolySupport.Vec d) => P.2 }

theorem HCPolySupport.HighContrast.isBlockMuAdmissible_constBlockState {d : ℕ} (U : Set (Vec d)) (P : BlockVec d) : IsBlockMuAdmissible U P (constBlockState P)

theorem HCPolySupport.HighContrast.zero_le_volumeAverage_blockEnergyDensity {d : ℕ} (U : Set (Vec d)) (a : CoeffSpace d) (X : BlockState d) : 0 ≤ volumeAverage U (blockEnergyDensity (↑↑a) X)

Every competitor over the coefficient space has nonnegative averaged energy.

theorem HCPolySupport.HighContrast.bddBelow_muValueSet {d : ℕ} (U : Set (Vec d)) (P : BlockVec d) (a : CoeffSpace d) : BddBelow (muValueSet U P ↑↑a)

theorem HCPolySupport.HighContrast.volumeAverage_blockEnergyDensity_constIdentity {d : ℕ} (U : Set (Vec d)) (P : BlockVec d) (hne : MeasureTheory.volume U ≠ 0) (hfin : MeasureTheory.volume U ≠ ⊤) : volumeAverage U (blockEnergyDensity (↑↑(constIdentity d)) (constBlockState P)) = 1 / 2 * blockNormSq P

At the constant identity field the constant competitor has averaged energy equal to half the doubled square norm of the boundary data, at every cube of finite positive volume.

theorem HCPolySupport.HighContrast.Mu_constIdentity_le {d : ℕ} (U : Set (Vec d)) (P : BlockVec d) (hne : MeasureTheory.volume U ≠ 0) (hfin : MeasureTheory.volume U ≠ ⊤) : Mu U P ↑↑(constIdentity d) ≤ 1 / 2 * blockNormSq P

The scale-uniform bound on the variational quantity of the constant identity field: the constant competitor is admissible at every cube.

The entries of the coarse response, and its quadratic form

theorem HCPolySupport.HighContrast.abs_blockMatEntry_coarseBlock_constIdentity_le {d : ℕ} (U : Set (Vec d)) (hne : MeasureTheory.volume U ≠ 0) (hfin : MeasureTheory.volume U ≠ ⊤) (α β : BlockCoord d) : |blockMatEntry (coarseBlock U (constIdentity d)) α β| ≤ 2

Every entry of the coarse response of the constant identity field is bounded by two, at every cube of finite positive volume.

theorem HCPolySupport.HighContrast.blockVecDot_le_of_abs_blockMatEntry_le {d : ℕ} (A : BlockMat d) (hA : ∀ (α β : BlockCoord d), |blockMatEntry A α β| ≤ 2) (X : BlockVec d) : blockVecDot X (blockMatVecMul A X) ≤ 4 * ↑d * blockNormSq X

A doubled block matrix with entries bounded by two has quadratic form bounded by 4d times the doubled square norm.

The reference block

def HCPolySupport.HighContrast.witnessRefBlock (d : ℕ) : BlockMat d

The reference block of the witness law: a positive multiple of the doubled identity, dimensional and free of every ellipticity constant.

Equations

• HCPolySupport.HighContrast.witnessRefBlock d = HCPolySupport.HighContrast.scaledBlockIdentity d (4 * ↑d + 1)

theorem HCPolySupport.HighContrast.isSymmetricBlockMat_witnessRefBlock {d : ℕ} : IsSymmetricBlockMat (witnessRefBlock d)

theorem HCPolySupport.HighContrast.blockPosDef_witnessRefBlock {d : ℕ} : Book.Ch02.BlockPosDef (witnessRefBlock d)

Cube volumes

theorem HCPolySupport.HighContrast.volume_standardCell_ne_zero {d : ℕ} (k : ℤ) (w : Fin d → ℤ) : MeasureTheory.volume (standardCell d k w) ≠ 0

theorem HCPolySupport.HighContrast.volume_standardCell_ne_top {d : ℕ} (k : ℤ) (w : Fin d → ℤ) : MeasureTheory.volume (standardCell d k w) ≠ ⊤

theorem HCPolySupport.HighContrast.blockScale_scaledBlockIdentity {d : ℕ} (c r : ℝ) : blockScale c (scaledBlockIdentity d r) = scaledBlockIdentity d (c * r)

theorem HCPolySupport.HighContrast.blockMatLoewnerLE_coarseBlock_constIdentity {d : ℕ} (k : ℤ) (w : Fin d → ℤ) : BlockMatLoewnerLE (coarseBlock (standardCell d k w) (constIdentity d)) (witnessRefBlock d)

The uniform domination. The coarse response of the constant identity field at every standard aligned cube, at every scale, is dominated by the reference block in the Loewner order — with no discount factor.

theorem HCPolySupport.HighContrast.blockMatLoewnerLE_coarseBlock_constIdentity_blockScale {d : ℕ} {c : ℝ} (hc : 1 ≤ c) (k : ℤ) (w : Fin d → ℤ) : BlockMatLoewnerLE (coarseBlock (standardCell d k w) (constIdentity d)) (blockScale c (witnessRefBlock d))

The domination survives every dilation of the reference block by a factor at least one, so it holds with the discount factor 3^{g(m-k)} of e.coarse.ellipticity at every nonnegative exponent.