High-contrast homogenization: Provider.Response.AffineResponseIdentification

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

Annealed identifications for affine reference responses

The common affine family represents both the terminal response and every aligned child response. Integer-translation stationarity identifies each child expectation with the centered physical response at the same scale. The reference partition defect therefore has exactly the physical response-defect expectation.

Terminal and aligned-cell identifications

theorem HCPolySupport.HighContrast.Response.integral_affineSubSkewResponseJ_eq_physical {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) (g : Mat d) (hg : IsSkewMat g) (A : CoeffSpace d → Book.Ch02.TriadicCoeffFamily d) (hA : ∀ (a : CoeffSpace d) (Q : TriadicCube d), ((A a).coeffOn Q).toCoeffField = affineCoefficient q ⋯ ((a.subSkew g hg).coeffOn (adaptedDomain hq t)).toCoeffField) (p r : Vec d) : ∫ (a : CoeffSpace d), Book.Ch02.responseJ (Book.Ch02.cubeDomain (originCube d t)) ((A a).coeffOn (originCube d t)) (matVecMul (matTranspose q) p) (matVecMul q⁻¹ r) ∂P = ∫ (a : CoeffSpace d), Book.Ch02.responseJ (adaptedDomain hq t) ((a.subSkew g hg).coeffOn (adaptedDomain hq t)) p r ∂P

The terminal response of the primal affine family is the physical recentered response at the untransformed loads.

theorem HCPolySupport.HighContrast.Response.integral_affineAdjointSubSkewResponseJ_eq_physical {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) (g : Mat d) (hg : IsSkewMat g) (A : CoeffSpace d → Book.Ch02.TriadicCoeffFamily d) (hA : ∀ (a : CoeffSpace d) (Q : TriadicCube d), ((A a).coeffOn Q).toCoeffField = affineCoefficient q ⋯ ((a.subSkew g hg).transpose.coeffOn (adaptedDomain hq t)).toCoeffField) (p r : Vec d) : ∫ (a : CoeffSpace d), Book.Ch02.responseJ (Book.Ch02.cubeDomain (originCube d t)) ((A a).coeffOn (originCube d t)) (matVecMul (matTranspose q) p) (matVecMul q⁻¹ r) ∂P = ∫ (a : CoeffSpace d), Book.Ch02.responseJ (adaptedDomain hq t) ((a.subSkew g hg).transpose.coeffOn (adaptedDomain hq t)) p r ∂P

The terminal response identification for the independently transported adjoint coefficient.

theorem HCPolySupport.HighContrast.Response.integral_affineSubSkewCellResponseJ_eq_physical {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} (hP : IsStationaryLaw P) {q : Mat d} (hq : Matrix.PosDef q) {l k t : ℤ} (hqGrid : IsRoundedGrid l q) (hlk : l ≤ k) (w : Fin d → ℤ) (g : Mat d) (hg : IsSkewMat g) (A : CoeffSpace d → Book.Ch02.TriadicCoeffFamily d) (hA : ∀ (a : CoeffSpace d) (Q : TriadicCube d), ((A a).coeffOn Q).toCoeffField = affineCoefficient q ⋯ ((a.subSkew g hg).coeffOn (adaptedDomain hq t)).toCoeffField) (p r : Vec d) (hbase : MeasureTheory.Integrable (fun (a : CoeffSpace d) => Book.Ch02.responseJ (adaptedDomain hq k) ((a.subSkew g hg).coeffOn (adaptedDomain hq k)) p r) P) : ∫ (a : CoeffSpace d), Book.Ch02.responseJ (Book.Ch02.cubeDomain (translateCube w (originCube d k))) ((A a).coeffOn (translateCube w (originCube d k))) (matVecMul (matTranspose q) p) (matVecMul q⁻¹ r) ∂P = ∫ (a : CoeffSpace d), Book.Ch02.responseJ (adaptedDomain hq k) ((a.subSkew g hg).coeffOn (adaptedDomain hq k)) p r ∂P

Every aligned primal reference child has the expectation of the centered physical response at its scale.

theorem HCPolySupport.HighContrast.Response.integral_affineAdjointSubSkewCellResponseJ_eq_physical {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} (hP : IsStationaryLaw P) {q : Mat d} (hq : Matrix.PosDef q) {l k t : ℤ} (hqGrid : IsRoundedGrid l q) (hlk : l ≤ k) (w : Fin d → ℤ) (g : Mat d) (hg : IsSkewMat g) (A : CoeffSpace d → Book.Ch02.TriadicCoeffFamily d) (hA : ∀ (a : CoeffSpace d) (Q : TriadicCube d), ((A a).coeffOn Q).toCoeffField = affineCoefficient q ⋯ ((a.subSkew g hg).transpose.coeffOn (adaptedDomain hq t)).toCoeffField) (p r : Vec d) (hbase : MeasureTheory.Integrable (fun (a : CoeffSpace d) => Book.Ch02.responseJ (adaptedDomain hq k) ((a.subSkew g hg).transpose.coeffOn (adaptedDomain hq k)) p r) P) : ∫ (a : CoeffSpace d), Book.Ch02.responseJ (Book.Ch02.cubeDomain (translateCube w (originCube d k))) ((A a).coeffOn (translateCube w (originCube d k))) (matVecMul (matTranspose q) p) (matVecMul q⁻¹ r) ∂P = ∫ (a : CoeffSpace d), Book.Ch02.responseJ (adaptedDomain hq k) ((a.subSkew g hg).transpose.coeffOn (adaptedDomain hq k)) p r ∂P

The aligned-cell expectation identity for the independent adjoint response.

The partition defect at the physical response defect

theorem HCPolySupport.HighContrast.Response.integral_affineSubSkewResponseJPartitionDefect_eq_profilePrimal {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} (hP : IsStationaryLaw P) {q : Mat d} (hq : Matrix.PosDef q) {l s t : ℤ} (hqGrid : IsRoundedGrid l q) (hls : l ≤ s) (j : ℕ) (hscale : t - ↑j = s) (g : Mat d) (hg : IsSkewMat g) (A : CoeffSpace d → Book.Ch02.TriadicCoeffFamily d) (hA : ∀ (a : CoeffSpace d) (Q : TriadicCube d), ((A a).coeffOn Q).toCoeffField = affineCoefficient q ⋯ ((a.subSkew g hg).coeffOn (adaptedDomain hq t)).toCoeffField) (p r : Vec d) (hchildInt : ∀ R ∈ descendantsAtDepth (originCube d t) j, MeasureTheory.Integrable (fun (a : CoeffSpace d) => Book.Ch02.responseJ (Book.Ch02.cubeDomain R) ((A a).coeffOn R) (matVecMul (matTranspose q) p) (matVecMul q⁻¹ r)) P) (hs : MeasureTheory.Integrable (fun (a : CoeffSpace d) => Book.Ch02.responseJ (adaptedDomain hq s) ((a.subSkew g hg).coeffOn (adaptedDomain hq s)) p r) P) (ht : MeasureTheory.Integrable (fun (a : CoeffSpace d) => Book.Ch02.responseJ (adaptedDomain hq t) ((a.subSkew g hg).coeffOn (adaptedDomain hq t)) p r) P) : ∫ (a : CoeffSpace d), Book.Ch05.Section53.JUpperBoundWeakNorms.responseJPartitionDefectOnFamilyAtDepth (A a) (originCube d t) j (matVecMul (matTranspose q) p) (matVecMul q⁻¹ r) ∂P = profilePrimalResponseDefect P hq g hg s t p r

The primal affine reference partition defect has exactly the physical primal response-defect expectation.

theorem HCPolySupport.HighContrast.Response.integral_affineAdjointSubSkewResponseJPartitionDefect_eq_profileAdjoint {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} (hP : IsStationaryLaw P) {q : Mat d} (hq : Matrix.PosDef q) {l s t : ℤ} (hqGrid : IsRoundedGrid l q) (hls : l ≤ s) (j : ℕ) (hscale : t - ↑j = s) (g : Mat d) (hg : IsSkewMat g) (A : CoeffSpace d → Book.Ch02.TriadicCoeffFamily d) (hA : ∀ (a : CoeffSpace d) (Q : TriadicCube d), ((A a).coeffOn Q).toCoeffField = affineCoefficient q ⋯ ((a.subSkew g hg).transpose.coeffOn (adaptedDomain hq t)).toCoeffField) (p r : Vec d) (hchildInt : ∀ R ∈ descendantsAtDepth (originCube d t) j, MeasureTheory.Integrable (fun (a : CoeffSpace d) => Book.Ch02.responseJ (Book.Ch02.cubeDomain R) ((A a).coeffOn R) (matVecMul (matTranspose q) p) (matVecMul q⁻¹ r)) P) (hs : MeasureTheory.Integrable (fun (a : CoeffSpace d) => Book.Ch02.responseJ (adaptedDomain hq s) ((a.subSkew g hg).transpose.coeffOn (adaptedDomain hq s)) p r) P) (ht : MeasureTheory.Integrable (fun (a : CoeffSpace d) => Book.Ch02.responseJ (adaptedDomain hq t) ((a.subSkew g hg).transpose.coeffOn (adaptedDomain hq t)) p r) P) : ∫ (a : CoeffSpace d), Book.Ch05.Section53.JUpperBoundWeakNorms.responseJPartitionDefectOnFamilyAtDepth (A a) (originCube d t) j (matVecMul (matTranspose q) p) (matVecMul q⁻¹ r) ∂P = profileAdjointResponseDefect P hq g hg s t p r

The same partition-defect identification for the independently transported adjoint response.