High-contrast homogenization: Provider.Response.DiagonalWeakNormComparison

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

Matrix comparisons for the diagonal weak norm

The estimates in this file compare the diagonal metric, a positive reference block, and the coarse response of an aligned cell. They also record positivity of the normalized averaged defect from exact aligned subadditivity.

Positivity of the diagonal metric

theorem HCPolySupport.HighContrast.Response.isSymmetricBlockMat_diagonalMetric {d : ℕ} {m0 : Mat d} (hm0 : Matrix.PosDef m0) : IsSymmetricBlockMat (Book.Ch02.blockDiag m0 m0⁻¹)

The block M₀ = diag(m₀,m₀⁻¹) is symmetric.

theorem HCPolySupport.HighContrast.Response.blockPosDef_diagonalMetric {d : ℕ} {m0 : Mat d} (hm0 : Matrix.PosDef m0) : Book.Ch02.BlockPosDef (Book.Ch02.blockDiag m0 m0⁻¹)

The block M₀ = diag(m₀,m₀⁻¹) is positive definite.

theorem HCPolySupport.HighContrast.Response.isSymmetricBlockMat_blockIdentity {d : ℕ} : IsSymmetricBlockMat (Book.Ch02.blockIdentity d)

The structural doubled identity is symmetric.

theorem HCPolySupport.HighContrast.Response.blockPosDef_blockIdentity {d : ℕ} : Book.Ch02.BlockPosDef (Book.Ch02.blockIdentity d)

The structural doubled identity is positive definite.

Squares of the printed factors

theorem HCPolySupport.HighContrast.Response.sq_diagonalWeakMetricFactor {d : ℕ} {m0 : Mat d} {E : BlockMat d} (hm0 : Matrix.PosDef m0) (hE : IsSymmetricBlockMat E) : diagonalWeakMetricFactor m0 E ^ 2 = blockSize E (Book.Ch02.blockDiag m0 m0⁻¹)

The square of K_{M,E} is the relative block size it names.

theorem HCPolySupport.HighContrast.Response.sq_diagonalWeakLoadMinus {d : ℕ} {E : BlockMat d} {p q : Vec d} (hE : IsSymmetricBlockMat E) (hEpd : Book.Ch02.BlockPosDef E) : diagonalWeakLoadMinus E p q ^ 2 = blockVecDot (-p, q) (blockMatVecMul E (-p, q))

The square of the primal load factor is the reference quadratic form.

theorem HCPolySupport.HighContrast.Response.sq_diagonalWeakLoadPlus {d : ℕ} {E : BlockMat d} {p q : Vec d} (hE : IsSymmetricBlockMat E) (hEpd : Book.Ch02.BlockPosDef E) : diagonalWeakLoadPlus E p q ^ 2 = blockVecDot (p, q) (blockMatVecMul E (p, q))

The square of the adjoint load factor is the reference quadratic form.

Positivity of the recent averaged defect

theorem HCPolySupport.HighContrast.Response.toFullBlockMat_diagonalWeakAverageDefect {d : ℕ} (q : Mat d) (k t : ℤ) (E : BlockMat d) (a : CoeffSpace d) : toFullBlockMat (diagonalWeakAverageDefect q k t E a) = (↑(alignedIndex q k t).card)⁻¹ • ∑ w ∈ alignedIndex q k t, toFullBlockMat (normalizedBlock (blockSub (adaptedResponse q k w a) (coarseBlock (adaptedCell q t) a)) E)

Flattening the averaged defect gives the printed average of the normalized cell defects.

theorem HCPolySupport.HighContrast.Response.toFullBlockMat_diagonalWeakAverageDefect_eq_normalized {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) {k t : ℤ} (hkt : k ≤ t) (E : BlockMat d) (a : CoeffSpace d) : toFullBlockMat (diagonalWeakAverageDefect q k t E a) = toFullBlockMat (normalizedBlock (blockSub (ofFullBlockMat ((↑(alignedIndex q k t).card)⁻¹ • ∑ w ∈ alignedIndex q k t, toFullBlockMat (adaptedResponse q k w a))) (coarseBlock (adaptedCell q t) a)) E)

Linearity identifies the printed average with the normalized difference between the aligned response average and the parent response.

theorem HCPolySupport.HighContrast.Response.posSemidef_diagonalWeakAverageDefect {d : ℕ} [NeZero d] {q : Mat d} (hq : Matrix.PosDef q) {k t : ℤ} (hkt : k ≤ t) {E : BlockMat d} (hE : IsSymmetricBlockMat E) (hEpd : Book.Ch02.BlockPosDef E) (a : CoeffSpace d) : Matrix.PosSemidef (toFullBlockMat (diagonalWeakAverageDefect q k t E a))

Exact aligned subadditivity makes D_{k,t}(E) positive semidefinite.

theorem HCPolySupport.HighContrast.Response.isSymmetricBlockMat_diagonalWeakAverageDefect {d : ℕ} [NeZero d] {q : Mat d} (hq : Matrix.PosDef q) {k t : ℤ} (hkt : k ≤ t) {E : BlockMat d} (hE : IsSymmetricBlockMat E) (hEpd : Book.Ch02.BlockPosDef E) (a : CoeffSpace d) : IsSymmetricBlockMat (diagonalWeakAverageDefect q k t E a)

The averaged defect is structurally symmetric.

theorem HCPolySupport.HighContrast.Response.blockSize_diagonalWeakAverageDefect_nonneg {d : ℕ} [NeZero d] {q : Mat d} (hq : Matrix.PosDef q) {k t : ℤ} (hkt : k ≤ t) {E : BlockMat d} (hE : IsSymmetricBlockMat E) (hEpd : Book.Ch02.BlockPosDef E) (a : CoeffSpace d) : 0 ≤ blockSize (diagonalWeakAverageDefect q k t E a) (Book.Ch02.blockIdentity d)

The scalar norm of a positive averaged defect is nonnegative.

The average comparison inequality

theorem HCPolySupport.HighContrast.Response.centered_metric_quadratic_le {d : ℕ} {M E D : FullBlockMat d} (hM : Matrix.PosDef M) (hE : Matrix.PosDef E) (x : FullBlockVec d) : Matrix.mulVec D x ⬝ᵥ M⁻¹.mulVec (Matrix.mulVec D x) ≤ relSize E M * ‖matSqrt E⁻¹ * D * matSqrt E⁻¹‖ ^ 2 * x ⬝ᵥ Matrix.mulVec E x

A centered symmetric block measured against E obeys the comparison quadratic form used in the comparison of the optimizer averages of two cells.

theorem HCPolySupport.HighContrast.Response.metricNormSq_blockAverage_sub_adapted_le {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) (k t : ℤ) (w : Fin d → ℤ) {a : CoeffSpace d} {c : Book.Ch02.CoeffOn (adaptedDomainAt hq k w)} {b : Book.Ch02.CoeffOn (adaptedDomain hq t)} {m : Mat d} (hm : Matrix.PosDef m) {E : BlockMat d} (hE : IsSymmetricBlockMat E) (hEpd : Book.Ch02.BlockPosDef E) (hc : Book.Ch02.coarseBlockMatrix (adaptedDomainAt hq k w) c = adaptedResponse q k w a) (hb : Book.Ch02.coarseBlockMatrix (adaptedDomain hq t) b = coarseBlock (adaptedCell q t) a) {p₀ q₀ : Vec d} {v : Book.Ch02.Solution (adaptedDomainAt hq k w) c} {u : Book.Ch02.Solution (adaptedDomain hq t) b} (hv : Book.Ch02.IsResponseMaximizer (adaptedDomainAt hq k w) c p₀ q₀ v) (hu : Book.Ch02.IsResponseMaximizer (adaptedDomain hq t) 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 t) b u, Book.Ch02.averageFlux (adaptedDomain hq t) 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 t) b u, Book.Ch02.averageFlux (adaptedDomain hq t) b u))) ≤ diagonalWeakMetricFactor m E ^ 2 * diagonalWeakLoadMinus E p₀ q₀ ^ 2 * blockSize (blockSub (adaptedResponse q k w a) (coarseBlock (adaptedCell q t) a)) E ^ 2

The exact aligned-cell comparison is bounded by the metric factor, the primal load factor, and the normalized response defect.