High-contrast homogenization: Provider.Response.DomainBridge

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

The adapted cell as a variational domain

The variational layer of Armstrong–Kuusi Chapter 2 — existence and uniqueness of the response maximizer, the first and second variation, the average identities, the energy identity, quadraticity, the block matrix formula and its row-swapped inverse, the doubled splitting and the doubled response space, the coarse graining estimates, and the scaling identities — is stated over an arbitrary nonempty bounded open convex domain. The adapted cells ⋄_k^q = q□_k and z + ⋄_k^q of a rounded geometry (s.scale.selection) are such domains, so the whole layer is available on them with no adaptation at all.

This file records that. It packages an adapted cell as a Chapter 2 domain and transports each of the fourteen theory bundles to the two adapted cells the response argument uses: the parent cell U_t = q□_t and the aligned child cell U_k(z) = z + q□_k, z ∈ 3^k𝕃_q. Downstream files quote the specializations below and never rebuild the domain.

Two clauses inside those bundles do not survive the move, and neither is used here. BlockCoarseMatrixTheory.block_matrix_subadditive, BlockCoarseMatrixTheory.starred_inverse_subadditive and ResponseSubadditivityAndScalingTheory.responseJ_subadditive quantify over a Book.Ch02.DomainPartition, whose realization clause forces the parent to be an open triadic cube subdivided into triadic descendants; over an adapted cell of a general grid q there is no such partition and the three clauses carry no content. The subadditivity the paper uses is instead the arbitrary almost everywhere partition into convex cells, Recurrence.blockQuadratic_le_sum_weight_of_- aePartition, and its instance at the aligned subdivision, Recurrence.toFullBlockMat_coarseBlock_adaptedCell_le_average.

The two adapted domains

def HCPolySupport.HighContrast.Response.adaptedDomain {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) (k : ℤ) : Book.Ch02.Domain d

The adapted cell ⋄_k^q = q□_k of a rounded geometry, as a Chapter 2 domain: it is open, bounded, convex and nonempty because q is positive definite.

Equations

• HCPolySupport.HighContrast.Response.adaptedDomain hq k = { carrier := HCPolySupport.HighContrast.adaptedCell q k, isDomain := ⋯, nonempty := ⋯ }

@[simp]

theorem HCPolySupport.HighContrast.Response.adaptedDomain_carrier {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) (k : ℤ) : (adaptedDomain hq k).carrier = adaptedCell q k

def HCPolySupport.HighContrast.Response.adaptedDomainAt {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) (k : ℤ) (w : Fin d → ℤ) : Book.Ch02.Domain d

The aligned adapted cell z + ⋄_k^q with z = 3^kqw ∈ 3^k𝕃_q, as a Chapter 2 domain.

Equations

• HCPolySupport.HighContrast.Response.adaptedDomainAt hq k w = { carrier := HCPolySupport.HighContrast.adaptedCellAt q k w, isDomain := ⋯, nonempty := ⋯ }

@[simp]

theorem HCPolySupport.HighContrast.Response.adaptedDomainAt_carrier {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) (k : ℤ) (w : Fin d → ℤ) : (adaptedDomainAt hq k w).carrier = adaptedCellAt q k w

theorem HCPolySupport.HighContrast.Response.adaptedDomainAt_subset {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) {j p : ℤ} (hjp : j ≤ p) {w : Fin d → ℤ} (hmem : adaptedCellCenter q j w ∈ adaptedCell q p) : (adaptedDomainAt hq j w).carrier ⊆ (adaptedDomain hq p).carrier

An aligned cell of the subdivision sits inside the parent cell, as domains: the containment of the adapted cells at the level of Chapter 2 domains.

The fourteen theories on the parent cell q□_k

The fourteen theories on an aligned cell z + q□_k