High-contrast homogenization: Provider.Quenched.SmallContrastDesignConstantBounds

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

The design instantiation's two constant bounds

The recursion constant of the endpoint is read at the isotropy carriers, and two of its arguments still name the reference block: the drop constant, whose value is the relative size of the block inside its own scalar multiple, and — through it — the recursion constant itself. Both are bounded by dimension-only numbers.

• the relative size of a block inside c times itself is at most c⁻¹, so the drop constant at the isotropy reference is at most 4;
• the recursion constant is monotone in the drop slot, so replacing the drop constant by 4 only enlarges it.

Together these are what lets the endpoint fix its decay rate before the reference block exists.

1. The relative size inside a scalar multiple

theorem HCPolySupport.HighContrast.Quenched.blockSize_blockScale_self_le {d : ℕ} {E : BlockMat d} (hE : IsSymmetricBlockMat E) (hEpd : Book.Ch02.BlockPosDef E) {c : ℝ} (hc : 0 < c) : blockSize E (blockScale c E) ≤ c⁻¹

A block inside a positive multiple of itself. The relative size is at most the reciprocal of the multiple.

theorem HCPolySupport.HighContrast.Quenched.dropConstantIsotropy_isotropyReference_le {d : ℕ} {E : BlockMat d} (hE : IsSymmetricBlockMat E) (hEpd : Book.Ch02.BlockPosDef E) {cIso : ℝ} (hcIso : 0 ≤ cIso) : dropConstantIsotropy (1 + cIso) E (isotropyReference cIso E) ≤ 4

The drop constant at the isotropy reference is at most four.

2. Monotonicity of the recursion constant in the drop slot

theorem HCPolySupport.HighContrast.Quenched.weakDropConstant_mono_cD {d : ℕ} {M L alpha cD cD' delta : ℝ} (halpha : 0 < alpha) (hdelta : 0 ≤ delta) (hcD : cD ≤ cD') : weakDropConstant M L alpha cD delta ≤ weakDropConstant M L alpha cD' delta

The drop-group constant is monotone in the drop constant.

theorem HCPolySupport.HighContrast.Quenched.fusionRecursionConstantIsotropySharp_mono_cD (d : ℕ) {Cpre eta : ℝ} (H : ℕ) {M L g cRow kap cD cD' delta cVsum cVm : ℝ} (hCpre : 0 ≤ Cpre) (hg1 : g < 1) (hdelta : 0 ≤ delta) (hcD : cD ≤ cD') : fusionRecursionConstantIsotropySharp d Cpre eta H M L g cRow kap cD delta cVsum cVm ≤ fusionRecursionConstantIsotropySharp d Cpre eta H M L g cRow kap cD' delta cVsum cVm

The recursion constant is monotone in the drop slot.