High-contrast homogenization: Provider.Response.DiagonalWeakNormRecentState

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

Local optimizers on the recent child cells

The recent-scale decomposition inserts the canonical optimizer on each aligned child. Its doubled state uses the same coefficient sample as the parent state and has the coarse-response average prescribed by the child block.

noncomputable def HCPolySupport.HighContrast.Response.diagonalWeakChildOptimizer {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) (k : ℤ) (w : Fin d → ℤ) (a : CoeffSpace d) (p r : Vec d) : Book.Ch02.Solution (adaptedDomainAt hq k w) (a.coeffOn (adaptedDomainAt hq k w))

The canonical optimizer v(U_k(z),p,r;a) on an aligned child cell.

Equations

• HCPolySupport.HighContrast.Response.diagonalWeakChildOptimizer hq k w a p r = (HCPolySupport.Book.Ch02.canonicalMaximizer ⋯ p r).toSolution

theorem HCPolySupport.HighContrast.Response.diagonalWeakChildOptimizer_isMaximizer {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) (k : ℤ) (w : Fin d → ℤ) (a : CoeffSpace d) (p r : Vec d) : Book.Ch02.IsResponseMaximizer (adaptedDomainAt hq k w) (a.coeffOn (adaptedDomainAt hq k w)) p r (diagonalWeakChildOptimizer hq k w a p r)

The child optimizer realizes the response functional at the printed load.

noncomputable def HCPolySupport.HighContrast.Response.diagonalWeakChildState {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) (k : ℤ) (w : Fin d → ℤ) (a : CoeffSpace d) (p r : Vec d) : Vec d → BlockVec d

The doubled child-optimizer state X(U_k(z)).

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.HighContrast.Response.diagonalWeakChildState_eq {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) (k : ℤ) (w : Fin d → ℤ) (a : CoeffSpace d) (p r x : Vec d) : diagonalWeakChildState hq k w a p r x = ((diagonalWeakChildOptimizer hq k w a p r).toH1.grad x, matVecMul ((a.coeffOn (adaptedDomainAt hq k w)).toCoeffField x) ((diagonalWeakChildOptimizer hq k w a p r).toH1.grad x))

Defining equation of the doubled child state.

theorem HCPolySupport.HighContrast.Response.blockCellAverage_diagonalWeakChildState {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) (k : ℤ) (w : Fin d → ℤ) (a : CoeffSpace d) (p r : Vec d) : blockCellAverage (adaptedCellAt q k w) (diagonalWeakChildState hq k w a p r) = (Book.Ch02.averageGradient (adaptedDomainAt hq k w) (a.coeffOn (adaptedDomainAt hq k w)) (diagonalWeakChildOptimizer hq k w a p r), Book.Ch02.averageFlux (adaptedDomainAt hq k w) (a.coeffOn (adaptedDomainAt hq k w)) (diagonalWeakChildOptimizer hq k w a p r))

The child-state average is the average-gradient/average-flux pair of its optimizer.

theorem HCPolySupport.HighContrast.Response.blockCellAverage_diagonalWeakChildState_eq_response {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) (k : ℤ) (w : Fin d → ℤ) (a : CoeffSpace d) (p r : Vec d) : blockCellAverage (adaptedCellAt q k w) (diagonalWeakChildState hq k w a p r) = blockMatVecMul (Book.Ch02.blockR d) (blockMatVecMul (adaptedResponse q k w a) (-p, r)) + (-p, r)

The child average is (R A_k(z)+I)(-p,r).

theorem HCPolySupport.HighContrast.Response.exists_diagonalWeakOptimizer_restrict_child {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) {k t : ℤ} (hkt : k ≤ t) {w : Fin d → ℤ} (hw : w ∈ alignedIndex q k t) (a : CoeffSpace d) (p r : Vec d) : ∃ (u : Book.Ch02.Solution (adaptedDomainAt hq k w) (a.coeffOn (adaptedDomainAt hq k w))), u.toH1.grad = (diagonalWeakOptimizer hq t a p r).toH1.grad

The parent optimizer restricts to a solution on each aligned child, with exactly the same gradient after transport through a shared pointwise coefficient representative.