High-contrast homogenization: Provider.Response.AlignedIdentities

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

The variational identities on the aligned subdivision

The identities of HCPoly.Provider.Response.VariationalIdentities and HCPoly.Provider.Response.EnergyMap are stated over an arbitrary Chapter 2 domain. This file supplies the two structural steps that the weak-norm estimate for the optimizer state performs on the aligned subdivision itself, and then reads every identity on the adapted parent cell U_t = q□_t and its aligned children U_k(z) = z + q□_k, with the paper's blocks A_t = 𝐀(U_t;a) and A_k(z) = 𝐀(U_k(z);a) in place of the Chapter 2 coarse block matrix.

The two structural steps are:

• restriction — "the primal and adjoint solutions representing Y remain solutions after restriction to every U_k(z)", and "the parent optimizer restricts to an admissible solution on every child: its equation holds against test functions supported in that child";
• membership — the doubled state X = (∇v, a∇v) of a solution lies in the response space 𝒮(V;a), and so does the difference X_t - X(U_k(z)) of two such states, because the difference of two a-harmonic functions is a-harmonic.

Both are stated with the pointwise ellipticity of the representative as a hypothesis; that is exactly what the coefficient bridge Response.exists_coeffOn_family produces for a sample of the law, simultaneously on the parent and on every aligned cell.

Solutions restrict to subdomains

theorem HCPolySupport.HighContrast.Response.weakFluxIntegrable_of_isEllipticFieldOn {d : ℕ} {U : Book.Ch02.Domain d} {lam Lam : ℝ} {a : Book.Ch02.CoeffOn U} (hEll : IsEllipticFieldOn lam Lam U.carrier a.toCoeffField) (u : Book.Ch02.Solution U a) : weakFluxIntegrable U.carrier a.toCoeffField u

The weak flux of a solution pairs integrably with every test gradient, on a domain carrying a pointwise elliptic representative.

theorem HCPolySupport.HighContrast.Response.exists_restrict_solution {d : ℕ} {U V : Book.Ch02.Domain d} {lam Lam : ℝ} {b : Book.Ch02.CoeffOn U} {c : Book.Ch02.CoeffOn V} (hrep : c.toCoeffField = b.toCoeffField) (hVU : V.carrier ⊆ U.carrier) (hEll : IsEllipticFieldOn lam Lam V.carrier c.toCoeffField) (u : Book.Ch02.Solution U b) : ∃ (z : Book.Ch02.Solution V c), z.toH1.grad = u.toH1.grad

The parent solution restricts to a subdomain: its equation holds against every test function supported in the subdomain, so its gradient is again an admissible solution gradient there.

theorem HCPolySupport.HighContrast.Response.exists_restrict_solution_adaptedCellAt {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) {j p : ℤ} (hjp : j ≤ p) {w : Fin d → ℤ} (hmem : adaptedCellCenter q j w ∈ adaptedCell q p) {lam Lam : ℝ} {b : Book.Ch02.CoeffOn (adaptedDomain hq p)} {c : Book.Ch02.CoeffOn (adaptedDomainAt hq j w)} (hrep : c.toCoeffField = b.toCoeffField) (hEll : IsEllipticFieldOn lam Lam (adaptedCellAt q j w) c.toCoeffField) (u : Book.Ch02.Solution (adaptedDomain hq p) b) : ∃ (z : Book.Ch02.Solution (adaptedDomainAt hq j w) c), z.toH1.grad = u.toH1.grad

The parent solution restricts to an aligned child cell of the adapted subdivision: the maximizer on U_p = q□_p restricts to a solution on U_j(z) = z + q□_j for every aligned centre z inside the parent.

theorem HCPolySupport.HighContrast.Response.exists_solution_grad_sub {d : ℕ} {U : Book.Ch02.Domain d} {lam Lam : ℝ} {a : Book.Ch02.CoeffOn U} (hEll : IsEllipticFieldOn lam Lam U.carrier a.toCoeffField) (u w : Book.Ch02.Solution U a) : ∃ (z : Book.Ch02.Solution U a), z.toH1.grad = fun (x : Vec d) => u.toH1.grad x - w.toH1.grad x

The difference of two solutions on the same domain is again a solution: the gradient difference is a-harmonic.

The doubled response space of a cell

theorem HCPolySupport.HighContrast.Response.isDoubledResponseField_gradFlux {d : ℕ} {U : Book.Ch02.Domain d} {a : Book.Ch02.CoeffOn U} (hEll : IsEllipticFieldOn a.lam a.Lam U.carrier a.toCoeffField) (v : Book.Ch02.Solution U a) : Book.Ch02.IsDoubledResponseField U a { potential := v.toH1.grad, flux := fun (x : Vec d) => matVecMul (a.toCoeffField x) (v.toH1.grad x) }

The doubled state of a solution lies in the response space: taking the adjoint solution to be zero in the description 𝒮(V;a) = {(∇u + ∇u^*, a∇u - aᵗ∇u^*)} gives X = (∇v, a∇v) ∈ 𝒮(V;a).

theorem HCPolySupport.HighContrast.Response.isDoubledResponseField_grad_sub {d : ℕ} {U : Book.Ch02.Domain d} {a : Book.Ch02.CoeffOn U} (hEll : IsEllipticFieldOn a.lam a.Lam U.carrier a.toCoeffField) (u w : Book.Ch02.Solution U a) : Book.Ch02.IsDoubledResponseField U a { potential := fun (x : Vec d) => u.toH1.grad x - w.toH1.grad x, flux := fun (x : Vec d) => matVecMul (a.toCoeffField x) (u.toH1.grad x) - matVecMul (a.toCoeffField x) (w.toH1.grad x) }

The difference of two optimizer states lies in the response space of the cell: "the parent optimizer restricts to an admissible solution on every child … thus X_t - X(U_k(z)) ∈ 𝒮(U_k(z);a)".

The identities read on the adapted cells

theorem HCPolySupport.HighContrast.Response.blockAverage_adaptedCellAt {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) (k : ℤ) (w : Fin d → ℤ) {a : CoeffSpace d} {c : Book.Ch02.CoeffOn (adaptedDomainAt hq k w)} (hc : Book.Ch02.coarseBlockMatrix (adaptedDomainAt hq k w) c = adaptedResponse q k w a) {p₀ q₀ : Vec d} {v : Book.Ch02.Solution (adaptedDomainAt hq k w) c} (hv : Book.Ch02.IsResponseMaximizer (adaptedDomainAt hq k w) c p₀ q₀ v) : (Book.Ch02.averageGradient (adaptedDomainAt hq k w) c v, Book.Ch02.averageFlux (adaptedDomainAt hq k w) c v) = blockMatVecMul (Book.Ch02.blockR d) (blockMatVecMul (adaptedResponse q k w a) (-p₀, q₀)) + (-p₀, q₀)

The average identity on an aligned cell, the average of the optimizer state at U_k(z): (X(U_k(z)))_{U_k(z)} = (RA_k(z) + I_{2d})P, with A_k(z) the adapted response block of that child cell.

theorem HCPolySupport.HighContrast.Response.blockAverage_adaptedCell {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) (p : ℤ) {a : CoeffSpace d} {b : Book.Ch02.CoeffOn (adaptedDomain hq p)} (hb : Book.Ch02.coarseBlockMatrix (adaptedDomain hq p) b = coarseBlock (adaptedCell q p) a) {p₀ q₀ : Vec d} {v : Book.Ch02.Solution (adaptedDomain hq p) b} (hv : Book.Ch02.IsResponseMaximizer (adaptedDomain hq p) b p₀ q₀ v) : (Book.Ch02.averageGradient (adaptedDomain hq p) b v, Book.Ch02.averageFlux (adaptedDomain hq p) b v) = blockMatVecMul (Book.Ch02.blockR d) (blockMatVecMul (coarseBlock (adaptedCell q p) a) (-p₀, q₀)) + (-p₀, q₀)

The average identity on the parent cell, the average of the optimizer state at U_t: (X_t)_{U_t} = (RA_t + I_{2d})P.

theorem HCPolySupport.HighContrast.Response.metricNormSq_blockAverage_sub_adapted {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) (k p : ℤ) (w : Fin d → ℤ) {a : CoeffSpace d} {c : Book.Ch02.CoeffOn (adaptedDomainAt hq k w)} {b : Book.Ch02.CoeffOn (adaptedDomain hq p)} (m : Mat d) (hc : Book.Ch02.coarseBlockMatrix (adaptedDomainAt hq k w) c = adaptedResponse q k w a) (hb : Book.Ch02.coarseBlockMatrix (adaptedDomain hq p) b = coarseBlock (adaptedCell q p) a) {p₀ q₀ : Vec d} {v : Book.Ch02.Solution (adaptedDomainAt hq k w) c} {u : Book.Ch02.Solution (adaptedDomain hq p) b} (hv : Book.Ch02.IsResponseMaximizer (adaptedDomainAt hq k w) c p₀ q₀ v) (hu : Book.Ch02.IsResponseMaximizer (adaptedDomain hq p) b p₀ q₀ u) : blockVecDot ((Book.Ch02.averageGradient (adaptedDomainAt hq k w) c v, Book.Ch02.averageFlux (adaptedDomainAt hq k w) c v) - (Book.Ch02.averageGradient (adaptedDomain hq p) b u, Book.Ch02.averageFlux (adaptedDomain hq p) b u)) (blockMatVecMul (Book.Ch02.blockDiag m m⁻¹) ((Book.Ch02.averageGradient (adaptedDomainAt hq k w) c v, Book.Ch02.averageFlux (adaptedDomainAt hq k w) c v) - (Book.Ch02.averageGradient (adaptedDomain hq p) b u, Book.Ch02.averageFlux (adaptedDomain hq p) b u))) = blockVecDot (blockMatVecMul (blockSub (adaptedResponse q k w a) (coarseBlock (adaptedCell q p) a)) (-p₀, q₀)) (blockMatVecMul (blockReflect (Book.Ch02.blockDiag m m⁻¹)) (blockMatVecMul (blockSub (adaptedResponse q k w a) (coarseBlock (adaptedCell q p) a)) (-p₀, q₀)))

The exact comparison identity across the aligned subdivision, the comparison of the optimizer averages at the pair (U_k(z), U_t): |M_0^{1/2}((X(U_k(z)))_{U_k(z)} - (X_t)_{U_t})|² = P·(A_k(z) - A_t)M_0^{-1}(A_k(z) - A_t)P, the block defect being exactly the one averaged in the recent cell defects C_{k,t}(E) and D_{k,t}(E).