High-contrast homogenization: Provider.Response.AffineAnnealedCutoffEnergy

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

Stationary cancellation for affine reference responses

An aligned reference child represents the response on its physical adapted image. Rounded-grid alignment makes that image an integer translate of the cell at the origin, so stationarity cancels the cutoff-weighted child response without placing a stationary law on the affine pullback family. The argument applies separately to the recentered coefficient and to its adjoint.

Literal primal and adjoint covariance

theorem HCPolySupport.HighContrast.Response.exists_translateCoeff_affineSubSkewResponseJ {d : ℕ} {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) : ∃ (z : Fin d → ℤ), ∀ (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) = Book.Ch02.responseJ (Book.Ch02.cubeDomain (originCube d k)) ((A (translateCoeff z a)).coeffOn (originCube d k)) (matVecMul (matTranspose q) p) (matVecMul q⁻¹ r)

A recentered affine reference child is the centered reference response of the translated physical sample.

theorem HCPolySupport.HighContrast.Response.exists_translateCoeff_affineAdjointSubSkewResponseJ {d : ℕ} {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) : ∃ (z : Fin d → ℤ), ∀ (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) = Book.Ch02.responseJ (Book.Ch02.cubeDomain (originCube d k)) ((A (translateCoeff z a)).coeffOn (originCube d k)) (matVecMul (matTranspose q) p) (matVecMul q⁻¹ r)

The adjoint recentered affine child obeys the same covariance, independently of the primal response.

Stationary cancellation

theorem HCPolySupport.HighContrast.Response.subSkew_neg_subSkew {d : ℕ} (a : CoeffSpace d) (g : Mat d) (hg : IsSkewMat g) : (a.subSkew g hg).subSkew (-g) ⋯ = a

noncomputable def HCPolySupport.HighContrast.Response.subSkewEquiv {d : ℕ} (g : Mat d) (hg : IsSkewMat g) : CoeffSpace d ≃ᵐ CoeffSpace d

Subtract a fixed skew matrix from a coefficient sample as a measurable equivalence, with inverse given by subtracting its negative.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HCPolySupport.HighContrast.Response.transposeEquiv {d : ℕ} : CoeffSpace d ≃ᵐ CoeffSpace d

Transpose coefficient samples as an involutive measurable equivalence.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HCPolySupport.HighContrast.Response.adjointSubSkewEquiv {d : ℕ} (g : Mat d) (hg : IsSkewMat g) : CoeffSpace d ≃ᵐ CoeffSpace d

The measurable equivalence that subtracts a fixed skew matrix and then transposes the resulting coefficient sample.

Equations

• HCPolySupport.HighContrast.Response.adjointSubSkewEquiv g hg = (HCPolySupport.HighContrast.Response.subSkewEquiv g hg).trans HCPolySupport.HighContrast.Response.transposeEquiv

theorem HCPolySupport.HighContrast.Response.integral_cutoffWeighted_affineSubSkewResponseJ_eq_zero {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} (hP : IsStationaryLaw P) {q : Mat d} (hq : Matrix.PosDef q) {l s t : ℤ} (hqGrid : IsRoundedGrid l q) (j : ℕ) (hscale : t - ↑j = s) (hls : l ≤ 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) {φ : Vec d → ℝ} (hint : ∀ 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) (hbase : 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) (hφ : MeasureTheory.IntegrableOn φ (cubeSet (originCube d t)) MeasureTheory.volume) (hmean : cubeAverage (originCube d t) φ = 1) : ∫ (a : CoeffSpace d), descendantsAverage (originCube d t) j fun (R : TriadicCube d) => (1 - cubeAverage R φ) * Book.Ch02.responseJ (Book.Ch02.cubeDomain R) ((A a).coeffOn R) (matVecMul (matTranspose q) p) (matVecMul q⁻¹ r) ∂P = 0

Under the physical stationary law, the cutoff-weighted responses of one compatible affine family for the recentered sample have mean zero.

theorem HCPolySupport.HighContrast.Response.integral_cutoffWeighted_affineAdjointSubSkewResponseJ_eq_zero {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} (hP : IsStationaryLaw P) {q : Mat d} (hq : Matrix.PosDef q) {l s t : ℤ} (hqGrid : IsRoundedGrid l q) (j : ℕ) (hscale : t - ↑j = s) (hls : l ≤ 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) {φ : Vec d → ℝ} (hint : ∀ 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) (hbase : 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) (hφ : MeasureTheory.IntegrableOn φ (cubeSet (originCube d t)) MeasureTheory.volume) (hmean : cubeAverage (originCube d t) φ = 1) : ∫ (a : CoeffSpace d), descendantsAverage (originCube d t) j fun (R : TriadicCube d) => (1 - cubeAverage R φ) * Book.Ch02.responseJ (Book.Ch02.cubeDomain R) ((A a).coeffOn R) (matVecMul (matTranspose q) p) (matVecMul q⁻¹ r) ∂P = 0

The same stationary cancellation for the independently transported adjoint recentered coefficient family.