High-contrast homogenization: Provider.Response.DiagonalWeakNormRecentAverage

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

The averaged optimizer-difference energy

The variational deficit on each recent child recombines over the exact partition. The affine load terms cancel, leaving twice the quadratic form of the averaged coarse-response defect.

theorem HCPolySupport.HighContrast.Response.diagonalWeak_child_difference_energy_eq_responseAverage {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) : (Book.Ch02.average (adaptedDomainAt hq k w) fun (x : Vec d) => blockVecDot (diagonalWeakChildState hq k w a p r x - diagonalWeakState hq t a p r x) (blockMatVecMul (blockMatrixOfCoeff (↑↑a x)) (diagonalWeakChildState hq k w a p r x - diagonalWeakState hq t a p r x))) = 4 * (Book.Ch02.responseJ (adaptedDomainAt hq k w) (a.coeffOn (adaptedDomainAt hq k w)) p r - volumeAverage (adaptedCellAt q k w) (Book.Ch02.responseIntegrand (adaptedDomain hq t) (a.coeffOn (adaptedDomain hq t)) p r (diagonalWeakOptimizer hq t a p r)))

The difference energy on one child is four times its response deficit, with the restricted parent value written as the child average of the parent integrand.

theorem HCPolySupport.HighContrast.Response.diagonalWeak_recent_energy_eq_response_deficit {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) {k t : ℤ} (hkt : k ≤ t) (a : CoeffSpace d) (p r : Vec d) : (avsum (alignedIndex q k t) fun (w : Fin d → ℤ) => Book.Ch02.average (adaptedDomainAt hq k w) fun (x : Vec d) => blockVecDot (diagonalWeakChildState hq k w a p r x - diagonalWeakState hq t a p r x) (blockMatVecMul (blockMatrixOfCoeff (↑↑a x)) (diagonalWeakChildState hq k w a p r x - diagonalWeakState hq t a p r x))) = 4 * ((avsum (alignedIndex q k t) fun (w : Fin d → ℤ) => Book.Ch02.responseJ (adaptedDomainAt hq k w) (a.coeffOn (adaptedDomainAt hq k w)) p r) - Book.Ch02.responseJ (adaptedDomain hq t) (a.coeffOn (adaptedDomain hq t)) p r)

Averaging the child identities and recombining the parent integrand gives four times the averaged response deficit.

theorem HCPolySupport.HighContrast.Response.diagonalWeak_response_deficit_eq_blockQuadratic {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) {k t : ℤ} (hkt : k ≤ t) (a : CoeffSpace d) (p r : Vec d) : (avsum (alignedIndex q k t) fun (w : Fin d → ℤ) => Book.Ch02.responseJ (adaptedDomainAt hq k w) (a.coeffOn (adaptedDomainAt hq k w)) p r) - Book.Ch02.responseJ (adaptedDomain hq t) (a.coeffOn (adaptedDomain hq t)) p r = 1 / 2 * blockVecDot (-p, r) (blockMatVecMul (blockSub (ofFullBlockMat ((↑(alignedIndex q k t).card)⁻¹ • ∑ w ∈ alignedIndex q k t, toFullBlockMat (adaptedResponse q k w a))) (coarseBlock (adaptedCell q t) a)) (-p, r))

The averaged response deficit is one half of the quadratic form of the averaged coarse-response defect.

theorem HCPolySupport.HighContrast.Response.diagonalWeak_recent_difference_energy_eq {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) {k t : ℤ} (hkt : k ≤ t) (a : CoeffSpace d) (p r : Vec d) : (avsum (alignedIndex q k t) fun (w : Fin d → ℤ) => Book.Ch02.average (adaptedDomainAt hq k w) fun (x : Vec d) => blockVecDot (diagonalWeakChildState hq k w a p r x - diagonalWeakState hq t a p r x) (blockMatVecMul (blockMatrixOfCoeff (↑↑a x)) (diagonalWeakChildState hq k w a p r x - diagonalWeakState hq t a p r x))) = 2 * blockVecDot (-p, r) (blockMatVecMul (blockSub (ofFullBlockMat ((↑(alignedIndex q k t).card)⁻¹ • ∑ w ∈ alignedIndex q k t, toFullBlockMat (adaptedResponse q k w a))) (coarseBlock (adaptedCell q t) a)) (-p, r))

The exact factor-two identity for the recent optimizer-difference energy.