High-contrast homogenization: Geometry.CoarseSchurBridge

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

The Schur blocks of the coarse response, and their ordering

The variational coarse block 𝐀(U; a) of s.introduction is carried here as a BlockMat d over a plain subset of ℝ^d and a field of the coefficient space, and its Schur data is read off the four corners by schurSigma and schurSigmaStar. CoarseGraining's chapter 2 carries the same object over a nonempty bounded open convex domain and a coefficient object with its own ellipticity data, and names the same two matrices sigmaCoarse and sigmaStarCoarse, extracted from the response functional rather than from the corners. The ordering σ_* ≤ σ is proved there.

This file identifies the two readings, so that the ordering becomes available on the response of a field of the coefficient space.

Three steps. A field of the coefficient space is uniformly elliptic almost everywhere on all of ℝ^d, so it is a coefficient object on every domain, with the same representative: this is CoeffSpace.coeffOn. The two block matrices then agree, because both are characterized by the same quadratic identity μ(U, P; a) = ½ P · 𝐀 P for every doubled vector P, and that identity determines the matrix. Finally, on the assembled form 𝐀 = (b, -kᵗ σ_*⁻¹; -σ_*⁻¹ k, σ_*⁻¹) the corner formulas are algebra: inverting the lower-right corner returns σ_*, the Schur skew block is k once σ_*⁻¹ is invertible, and the correction kᵗ σ_*⁻¹ k subtracted from b returns σ.

A field of the coefficient space as a coefficient object on a domain

theorem HCPolySupport.HighContrast.CoeffSpace.exists_ellipticity_on_domain {d : ℕ} (a : CoeffSpace d) (U : Book.Ch02.Domain d) : ∃ (lam : ℝ) (Lam : ℝ), 0 < lam ∧ lam ≤ Lam ∧ ∀ᵐ (x : Vec d), x ∈ U.carrier → IsEllipticMatrix lam Lam (↑↑a x)

The ellipticity constants a field of the coefficient space carries on a bounded open convex domain.

noncomputable def HCPolySupport.HighContrast.CoeffSpace.coeffOn {d : ℕ} (a : CoeffSpace d) (U : Book.Ch02.Domain d) : Book.Ch02.CoeffOn U

A field of the coefficient space, viewed as a coefficient object on a nonempty bounded open convex domain: the ellipticity constants are the ones the field carries on that domain, and the representative is unchanged.

Equations

• a.coeffOn U = { toCoeffField := ↑↑a, lam := ⋯.choose, Lam := ⋯.choose, lam_pos := ⋯, lam_le_Lam := ⋯, aeStronglyMeasurable := ⋯, aeElliptic := ⋯ }

@[simp]

theorem HCPolySupport.HighContrast.CoeffSpace.coeffOn_toCoeffField {d : ℕ} (a : CoeffSpace d) (U : Book.Ch02.Domain d) : (a.coeffOn U).toCoeffField = ↑↑a

The two readings of the coarse block agree

theorem HCPolySupport.HighContrast.coarseBlock_eq_coarseBlockMatrix {d : ℕ} (a : CoeffSpace d) (U : Book.Ch02.Domain d) : coarseBlock U.carrier a = Book.Ch02.coarseBlockMatrix U (a.coeffOn U)

The coarse response is the chapter 2 coarse block matrix. Both are determined by the same quadratic identity for the variational quantity.

Positivity on general domains

theorem HCPolySupport.HighContrast.blockPosDef_coarseBlock_of_isOpenBoundedConvexDomain {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (hne : U.Nonempty) (a : CoeffSpace d) : Book.Ch02.BlockPosDef (coarseBlock U a)

The coarse response of a field of the coefficient space is positive definite on every bounded open convex nonempty domain: it is the chapter 2 coarse block matrix of the field read as a coefficient object on that domain.

The corner formulas

theorem HCPolySupport.HighContrast.schurSkew_blockMatrixOfCoarseMatrices {d : ℕ} {M : Book.Ch02.CoarseMatrices d} (hdet : IsUnit (Matrix.det M.sigmaStarInv)) : schurSkew (Book.Ch02.blockMatrixOfCoarseMatrices M) = M.kappa

The Schur skew block of the assembled block is k.

theorem HCPolySupport.HighContrast.schurSigma_blockMatrixOfCoarseMatrices {d : ℕ} {M : Book.Ch02.CoarseMatrices d} (hdet : IsUnit (Matrix.det M.sigmaStarInv)) : schurSigma (Book.Ch02.blockMatrixOfCoarseMatrices M) = M.sigma

The Schur symmetric block of the assembled block is σ: the correction kᵗ σ_*⁻¹ k is exactly what b adds to σ.

The Schur data of the coarse response

theorem HCPolySupport.HighContrast.schurSigmaStar_coarseBlock {d : ℕ} (a : CoeffSpace d) (U : Book.Ch02.Domain d) : schurSigmaStar (coarseBlock U.carrier a) = Book.Ch02.sigmaStarCoarse U (a.coeffOn U)

The Schur block σ_* of the coarse response is the chapter 2 matrix sigmaStarCoarse.

theorem HCPolySupport.HighContrast.schurSigma_coarseBlock {d : ℕ} (a : CoeffSpace d) (U : Book.Ch02.Domain d) (hpos : Book.Ch02.BlockPosDef (coarseBlock U.carrier a)) : schurSigma (coarseBlock U.carrier a) = Book.Ch02.sigmaCoarse U (a.coeffOn U)

The Schur block σ of the coarse response is the chapter 2 matrix sigmaCoarse.

The ordering

theorem HCPolySupport.HighContrast.matLoewnerLE_schurSigmaStar_schurSigma_coarseBlock {d : ℕ} (a : CoeffSpace d) (U : Book.Ch02.Domain d) (hpos : Book.Ch02.BlockPosDef (coarseBlock U.carrier a)) : MatLoewnerLE (schurSigmaStar (coarseBlock U.carrier a)) (schurSigma (coarseBlock U.carrier a))

The Schur blocks of the coarse response are ordered, σ_* ≤ σ, on every nonempty bounded open convex domain and at every field of the coefficient space.

theorem HCPolySupport.HighContrast.cubeDomain_originCube_coe {d : ℕ} (m : ℤ) : (Book.Ch02.cubeDomain (originCube d m)).carrier = centeredCube d m

The centered triadic cube □_m of s.introduction as a nonempty bounded open convex domain.

theorem HCPolySupport.HighContrast.matLoewnerLE_schurSigmaStar_schurSigma_coarseBlock_centeredCube {d : ℕ} [NeZero d] (m : ℤ) (a : CoeffSpace d) : MatLoewnerLE (schurSigmaStar (coarseBlock (centeredCube d m) a)) (schurSigma (coarseBlock (centeredCube d m) a))

The Schur blocks of the coarse response of a centered triadic cube are ordered, at every field of the coefficient space.

theorem HCPolySupport.HighContrast.one_le_aspectRatio_coarseBlock_centeredCube {d : ℕ} [NeZero d] (m : ℤ) (a : CoeffSpace d) : 1 ≤ aspectRatio (coarseBlock (centeredCube d m) a)

The aspect ratio of a realized coarse block is at least one. The Schur ordering holds on the coarse response of a centered triadic cube, so the bound of e.reference.aspect.ratio applies to it with no further hypothesis.