High-contrast homogenization: Geometry.ReferenceAspectRatio

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

The reference aspect ratio of e.coarse.ellipticity is at least one

The reference block E of the coarse ellipticity assumption dominates the coarse response of every standard aligned cube, with a discount factor 3^{g(m-k)} that is one at the scale of the cube itself. So E dominates the coarse response of a centered triadic cube at some field of the coefficient space, provided one such field is reachable — which is exactly what a probability law supplies, since the assumption's bound holds almost surely and the source scale S is finite at every field.

The Schur blocks of a realized coarse response are ordered, so its aspect ratio is at least one; the aspect ratio is monotone; hence 1 ≤ Π(E). This is the lower bound Θ ≥ 1 the reference text uses, obtained without assuming the ordering of the reference block itself.

The hypothesis that the law is a probability measure is not cosmetic: at the zero measure the assumption is satisfied by a reference block with Π = 1/4, because nothing is then reachable.

theorem HCPolySupport.HighContrast.blockScale_one {d : ℕ} (E : BlockMat d) : blockScale 1 E = E

The trivial dilation of a doubled block matrix.

theorem HCPolySupport.HighContrast.blockMatLoewnerLE_coarseBlock_centeredCube_of_coarseEllipticityDagger {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {g : ℝ} {E : BlockMat d} {Ψ : ℝ → ℝ} {K : ℝ} {S : CoeffSpace d → ℝ} (hdag : CoarseEllipticityDagger P g E Ψ K S) : ∀ᵐ (a : CoeffSpace d) ∂P, ∀ (m : ℤ), S a ≤ 3 ^ m → BlockMatLoewnerLE (coarseBlock (centeredCube d m) a) E

The assumption is undiscounted at the scale of the cube. Taking the standard aligned cube to be the centered cube itself makes the discount factor 3^{g(m-k)} equal to one, so e.coarse.ellipticity bounds the coarse response of □_m by the reference block.

theorem HCPolySupport.HighContrast.one_le_aspectRatio_of_coarseEllipticityDagger {d : ℕ} [NeZero d] {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {g : ℝ} {E : BlockMat d} {Ψ : ℝ → ℝ} {K : ℝ} {S : CoeffSpace d → ℝ} (hdag : CoarseEllipticityDagger P g E Ψ K S) : 1 ≤ aspectRatio E

The reference aspect ratio is at least one. Under e.coarse.ellipticity at a probability law, the reference block dominates the coarse response of a centered triadic cube at some field of the coefficient space; that response has ordered Schur blocks, hence aspect ratio at least one, and the aspect ratio is monotone.