High-contrast homogenization: Provider.Response.AnnealedDefectIdentification

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

The cellwise defects and the response defect

The defect half of a cutoff-defect mean row consumes a family of cell defects whose normalized average is twice the response defect. The response defect is defined as the expectation of a difference of two responses, while the cellwise data arrives as a difference of two expectations; the two agree once both responses are integrable.

This module records that identification, the normalized average that follows from it, and the nonnegativity of each cell defect in the same literal form. The geometry of the cells enters only through the hypothesis that every cell carries the same annealed response, which is what the alignment of the grid supplies.

Normalized averages of a function that is constant on its index set

theorem HCPolySupport.HighContrast.Response.avsum_eq_of_forall_eq {ι : Type u_1} {Z : Finset ι} (hZ : Z.Nonempty) {f : ι → ℝ} {c : ℝ} (hf : ∀ z ∈ Z, f z = c) : avsum Z f = c

A normalized average of a function that is constant on the index set is that constant.

The response defect as a difference of expectations

theorem HCPolySupport.HighContrast.Response.profilePrimalResponseDefect_eq_sub_integral {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) {q : Mat d} (hq : Matrix.PosDef q) (g : Mat d) (hg : IsSkewMat g) (s t : ℤ) (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) : profilePrimalResponseDefect P hq g hg s t p r = ∫ (a : CoeffSpace d), Book.Ch02.responseJ (adaptedDomain hq s) ((a.subSkew g hg).coeffOn (adaptedDomain hq s)) p r ∂P - ∫ (a : CoeffSpace d), Book.Ch02.responseJ (adaptedDomain hq t) ((a.subSkew g hg).coeffOn (adaptedDomain hq t)) p r ∂P

The primal response defect is a difference of expectations. The defect is defined as one expectation of a difference; splitting it needs both responses to be integrable.

theorem HCPolySupport.HighContrast.Response.profileAdjointResponseDefect_eq_sub_integral {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) {q : Mat d} (hq : Matrix.PosDef q) (g : Mat d) (hg : IsSkewMat g) (s t : ℤ) (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) : profileAdjointResponseDefect P hq g hg s t p r = ∫ (a : CoeffSpace d), Book.Ch02.responseJ (adaptedDomain hq s) ((a.subSkew g hg).transpose.coeffOn (adaptedDomain hq s)) p r ∂P - ∫ (a : CoeffSpace d), Book.Ch02.responseJ (adaptedDomain hq t) ((a.subSkew g hg).transpose.coeffOn (adaptedDomain hq t)) p r ∂P

The coefficient-transpose response defect as a difference of expectations.

The cellwise defects

The normalized average and the nonnegativity