High-contrast homogenization: Provider.Response.AffineResponseEnergyIdentification

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

Physical identification of affine difference energy

The affine reference family can be chosen samplewise from the physical coefficient. Stationarity transfers physical response integrability to every aligned reference child. Consequently the actual descendant-averaged parent--child half-energy has expectation equal to the physical response defect, for the primal and adjoint coefficients separately.

Actual energy identities

theorem HCPolySupport.HighContrast.Response.exists_integral_affineSubSkewDifferenceEnergy_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) (p r : Vec d) (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.Ch02.TriadicCoeffFamily d), (∀ (a : CoeffSpace d) (Q : TriadicCube d), ((A a).coeffOn Q).toCoeffField = affineCoefficient q ⋯ ((a.subSkew g hg).coeffOn (adaptedDomain hq t)).toCoeffField) ∧ (∀ 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) ∧ MeasureTheory.Integrable (fun (a : CoeffSpace d) => Book.Ch02.responseJ (Book.Ch02.cubeDomain (originCube d s)) ((A a).coeffOn (originCube d s)) (matVecMul (matTranspose q) p) (matVecMul q⁻¹ r)) P ∧ ∫ (a : CoeffSpace d), descendantsAverage (originCube d t) j fun (R : TriadicCube d) => cubeAverage R (Book.Ch05.Section53.JUpperBoundWeakNorms.additivityDiffHalfEnergyDensityOnFamilyOnCube (A a) (originCube d t) R (matVecMul (matTranspose q) p) (matVecMul q⁻¹ r)) ∂P = profilePrimalResponseDefect P hq g hg s t p r

There is a samplewise compatible primal affine family whose actual descendant-averaged difference half-energy has expectation equal to the physical primal response defect.

theorem HCPolySupport.HighContrast.Response.exists_integral_affineAdjointSubSkewDifferenceEnergy_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) (p r : Vec d) (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.Ch02.TriadicCoeffFamily d), (∀ (a : CoeffSpace d) (Q : TriadicCube d), ((A a).coeffOn Q).toCoeffField = affineCoefficient q ⋯ ((a.subSkew g hg).transpose.coeffOn (adaptedDomain hq t)).toCoeffField) ∧ (∀ 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) ∧ MeasureTheory.Integrable (fun (a : CoeffSpace d) => Book.Ch02.responseJ (Book.Ch02.cubeDomain (originCube d s)) ((A a).coeffOn (originCube d s)) (matVecMul (matTranspose q) p) (matVecMul q⁻¹ r)) P ∧ ∫ (a : CoeffSpace d), descendantsAverage (originCube d t) j fun (R : TriadicCube d) => cubeAverage R (Book.Ch05.Section53.JUpperBoundWeakNorms.additivityDiffHalfEnergyDensityOnFamilyOnCube (A a) (originCube d t) R (matVecMul (matTranspose q) p) (matVecMul q⁻¹ r)) ∂P = profileAdjointResponseDefect P hq g hg s t p r

The independently chosen adjoint affine family satisfies the same actual energy identity at the adjoint response defect.