Documentation

LeanPool.HighContrastHomogenization.Provider.Quenched.BlockScaleGeometry

High-contrast homogenization: Provider.Quenched.BlockScaleGeometry #

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

Scalar dilation of reference geometry #

This file records the homogeneity of the reference aspect ratio and the quadratic upper homogeneity of the intrinsic contrast under a positive common scalar dilation of a doubled block.

source
theorem HCPolySupport.HighContrast.Quenched.aspectRatio_blockScale {d : ℕ} {c : ℝ} (hc : 0 < c) (E : BlockMat d) :
aspectRatio (blockScale c E) = c ^ 2 * aspectRatio E

The reference aspect ratio is homogeneous of degree two under a common positive scalar dilation of a doubled block.

source
theorem HCPolySupport.HighContrast.Quenched.blockContrast_blockScale_le {d : ℕ} {B : BlockMat d} (hBsymm : IsSymmetricBlockMat B) (hBpos : Book.Ch02.BlockPosDef B) {c : ℝ} (hc : 0 < c) :
blockContrast (blockScale c B) ≤ c ^ 2 * blockContrast B

Intrinsic contrast grows by at most the square of a positive common scalar dilation.