High-contrast homogenization: Provider.Response.CoefficientBridge

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

The coefficient of a sample on an adapted cell

The variational layer of Armstrong–Kuusi Chapter 2 reads a coefficient field through the domain-local interface Book.Ch02.CoeffOn U: a representative together with a pair of ellipticity constants valid almost everywhere on U. The high-contrast paper instead carries a sample a of the coefficient law, an almost everywhere class, and reads its coarse block response 𝐀(U; a), the variational coarse block of s.introduction, through the variational block matrix of the class. This file connects the two.

The connection is uniform in the domain, and that is what makes it usable on a subdivision. A sample has a measurable representative that is elliptic at every point, and such a field is a Chapter 2 coefficient on every domain at once, with the same representative and the same constants; so the parent cell U_t = q□_t and all of its aligned children U_k(z) = z + q□_k may be equipped simultaneously, each child coefficient being literally the restriction of the parent one. On each of them the Chapter 2 coarse block matrix is the paper's own coarse block response: for the aligned cells this is the adapted response A_k(z) = 𝐀(U_k(z); a) of the child cell.

A pointwise elliptic field is a coefficient on every domain

theorem HCPolySupport.HighContrast.Response.exists_coeffOn_of_measurable {d : ℕ} {f : CoeffField d} {lam Lam : ℝ} (hlam : 0 < lam) (hle : lam ≤ Lam) (hfm : Measurable f) (U : Book.Ch02.Domain d) (hell : ∀ x ∈ U.carrier, IsEllipticMatrix lam Lam (f x)) : ∃ (b : Book.Ch02.CoeffOn U), b.toCoeffField = f ∧ b.lam = lam ∧ b.Lam = Lam ∧ IsEllipticFieldOn lam Lam U.carrier f

A measurable field that is elliptic at every point of a domain is a Chapter 2 coefficient on that domain, with its own representative and its own constants unchanged.

The representative of a sample

theorem HCPolySupport.HighContrast.Response.exists_representative {d : ℕ} (a : CoeffSpace d) {S : Set (Vec d)} (hS : Bornology.IsBounded S) : ∃ (f : CoeffField d) (lam : ℝ) (Lam : ℝ), 0 < lam ∧ lam ≤ Lam ∧ Measurable f ∧ (∀ x ∈ S, IsEllipticMatrix lam Lam (f x)) ∧ ∀ (U : Set (Vec d)), coarseBlock U a = coarseBlockMatrix U f

A sample of the coefficient law has a measurable representative, elliptic at every point of a prescribed bounded set, that computes the coarse block response of the sample on every set.

The Chapter 2 coarse block matrix is the coarse block response

theorem HCPolySupport.HighContrast.Response.coarseBlockMatrix_eq_of_isEllipticFieldOn {d : ℕ} [NeZero d] (U : Book.Ch02.Domain d) (b : Book.Ch02.CoeffOn U) (hEll : IsEllipticFieldOn b.lam b.Lam U.carrier b.toCoeffField) : Book.Ch02.coarseBlockMatrix U b = coarseBlockMatrix U.carrier b.toCoeffField

On a domain carrying an elliptic representative, the public Chapter 2 coarse block matrix 𝐀(U; a) agrees with the variational coarse block matrix of the representative.

The bridge on the adapted cells