High-contrast homogenization: Provider.Response.ProfileDefectIdentities

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

Identities and positivity for the response defects

Constant-skew covariance moves each recentered response to its corrected load. The annealed quadratic identities then identify the two defects with the corresponding recentered mean increments. Mean order gives their signs.

theorem HCPolySupport.HighContrast.Response.profileDefect_blockG_mulVec {d : ℕ} (g : Mat d) (X : BlockVec d) : blockMatVecMul (Book.Ch02.blockG g) X = (X.1, matVecMul g X.1 + X.2)

The structural shear sends (x,y) to (x,gx+y).

theorem HCPolySupport.HighContrast.Response.profileRecenteredMean_quadratic {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (q g : Mat d) (k : ℤ) (X : BlockVec d) : blockVecDot X (blockMatVecMul (profileRecenteredMean P q g k) X) = blockVecDot (blockMatVecMul (Book.Ch02.blockG g) X) (blockMatVecMul (adaptedMean P q k) (blockMatVecMul (Book.Ch02.blockG g) X))

A quadratic form of the recentered mean is the original quadratic form at the sheared load.

theorem HCPolySupport.HighContrast.Response.profileRecenteredAdjointMean_quadratic {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (q g : Mat d) (k : ℤ) (X : BlockVec d) : blockVecDot X (blockMatVecMul (profileRecenteredAdjointMean P q g k) X) = blockVecDot (blockMatVecMul (Book.Ch02.blockG g) (blockMatVecMul (Book.Ch02.blockDiag 1 (-1)) X)) (blockMatVecMul (adaptedMean P q k) (blockMatVecMul (Book.Ch02.blockG g) (blockMatVecMul (Book.Ch02.blockDiag 1 (-1)) X)))

A quadratic form of the recentered adjoint mean is the original quadratic form at the signed, sheared load.

theorem HCPolySupport.HighContrast.Response.profileRecenteredMean_le {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {q g : Mat d} {s t : ℤ} (hmean : BlockMatLoewnerLE (adaptedMean P q t) (adaptedMean P q s)) : BlockMatLoewnerLE (profileRecenteredMean P q g t) (profileRecenteredMean P q g s)

Recentered mean order is inherited from the original mean order.

theorem HCPolySupport.HighContrast.Response.profileRecenteredAdjointMean_le {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {q g : Mat d} {s t : ℤ} (hmean : BlockMatLoewnerLE (adaptedMean P q t) (adaptedMean P q s)) : BlockMatLoewnerLE (profileRecenteredAdjointMean P q g t) (profileRecenteredAdjointMean P q g s)

Recentered adjoint mean order is inherited from the original mean order.

theorem HCPolySupport.HighContrast.Response.profilePrimalResponseDefect_eq_corrected_integrals {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {q : Mat d} (hq : Matrix.PosDef q) {g : Mat d} (hg : IsSkewMat g) {s t : ℤ} (hints : HasFiniteAdaptedMean P q s) (hintt : HasFiniteAdaptedMean P q t) (p r : Vec d) : profilePrimalResponseDefect P hq g hg s t p r = ∫ (a : CoeffSpace d), Book.Ch02.responseJ (adaptedDomain hq s) (a.coeffOn (adaptedDomain hq s)) p (r - matVecMul g p) ∂P - ∫ (a : CoeffSpace d), Book.Ch02.responseJ (adaptedDomain hq t) (a.coeffOn (adaptedDomain hq t)) p (r - matVecMul g p) ∂P

Constant-skew covariance and integrability turn the primal expectation of a difference into the difference of the two corrected-load expectations.

theorem HCPolySupport.HighContrast.Response.profilePrimalResponseDefect_identity {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {q : Mat d} (hq : Matrix.PosDef q) {g : Mat d} (hg : IsSkewMat g) {s t : ℤ} (hints : HasFiniteAdaptedMean P q s) (hintt : HasFiniteAdaptedMean P q t) (p r : Vec d) : profilePrimalResponseDefect P hq g hg s t p r = 1 / 2 * blockVecDot (-p, r) (blockMatVecMul (blockSub (profileRecenteredMean P q g s) (profileRecenteredMean P q g t)) (-p, r))

The primal defect is exactly one half of the recentered mean-increment quadratic form.

theorem HCPolySupport.HighContrast.Response.profileAdjointResponseDefect_eq_corrected_integrals {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {q : Mat d} (hq : Matrix.PosDef q) {g : Mat d} (hg : IsSkewMat g) {s t : ℤ} (hints : HasFiniteAdaptedMean P q s) (hintt : HasFiniteAdaptedMean P q t) (p r : Vec d) : profileAdjointResponseDefect P hq g hg s t p r = ∫ (a : CoeffSpace d), Book.Ch02.responseJ (adaptedDomain hq s) (a.transpose.coeffOn (adaptedDomain hq s)) p (r + matVecMul g p) ∂P - ∫ (a : CoeffSpace d), Book.Ch02.responseJ (adaptedDomain hq t) (a.transpose.coeffOn (adaptedDomain hq t)) p (r + matVecMul g p) ∂P

Constant-skew covariance and integrability turn the adjoint expectation of a difference into the difference of its two corrected-load expectations.

theorem HCPolySupport.HighContrast.Response.profileAdjointResponseDefect_identity {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {q : Mat d} (hq : Matrix.PosDef q) {g : Mat d} (hg : IsSkewMat g) {s t : ℤ} (hints : HasFiniteAdaptedMean P q s) (hintt : HasFiniteAdaptedMean P q t) (p r : Vec d) : profileAdjointResponseDefect P hq g hg s t p r = 1 / 2 * blockVecDot (-p, r) (blockMatVecMul (blockSub (profileRecenteredAdjointMean P q g s) (profileRecenteredAdjointMean P q g t)) (-p, r))

The coefficient-transpose defect is exactly one half of the adjoint recentered mean-increment quadratic form.

theorem HCPolySupport.HighContrast.Response.profilePrimalResponseDefect_nonneg {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {q : Mat d} (hq : Matrix.PosDef q) {g : Mat d} (hg : IsSkewMat g) {s t : ℤ} (hints : HasFiniteAdaptedMean P q s) (hintt : HasFiniteAdaptedMean P q t) (hmean : BlockMatLoewnerLE (adaptedMean P q t) (adaptedMean P q s)) (p r : Vec d) : 0 ≤ profilePrimalResponseDefect P hq g hg s t p r

The primal response defect is nonnegative on an ordered scale pair.

theorem HCPolySupport.HighContrast.Response.profileAdjointResponseDefect_nonneg {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {q : Mat d} (hq : Matrix.PosDef q) {g : Mat d} (hg : IsSkewMat g) {s t : ℤ} (hints : HasFiniteAdaptedMean P q s) (hintt : HasFiniteAdaptedMean P q t) (hmean : BlockMatLoewnerLE (adaptedMean P q t) (adaptedMean P q s)) (p r : Vec d) : 0 ≤ profileAdjointResponseDefect P hq g hg s t p r

The coefficient-transpose response defect is nonnegative on an ordered scale pair.