High-contrast homogenization: Provider.Response.AffineResponseCongruence

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

Stationary cancellation after affine normalization

At an aligned scale, multiplying the adapted grid by the corresponding triadic factor gives an integer matrix. Affine normalization by that matrix therefore conjugates integer translations to integer translations and pushes a stationary coefficient law to another stationary law. The unconditional response congruence on ordinary triadic cubes can then be applied before transporting the response and cutoff averages back to the adapted affine family.

theorem HCPolySupport.HighContrast.Response.exists_affineCoeffSpace {d : ℕ} (L : Mat d) (hL : IsUnit (Matrix.det L)) (a : CoeffSpace d) : ∃ (b : CoeffSpace d), ↑↑b =ᵐ[MeasureTheory.volume] affineCoefficient L hL ↑↑a

noncomputable def HCPolySupport.HighContrast.Response.affineCoeffSpace {d : ℕ} (L : Mat d) (hL : IsUnit (Matrix.det L)) (a : CoeffSpace d) : CoeffSpace d

The coefficient-space sample representing the affine transform of a under the invertible matrix L, up to almost-everywhere equality.

Equations

• HCPolySupport.HighContrast.Response.affineCoeffSpace L hL a = ⋯.choose

theorem HCPolySupport.HighContrast.Response.measurable_affineCoeffSpace {d : ℕ} (L : Mat d) (hL : IsUnit (Matrix.det L)) : Measurable (affineCoeffSpace L hL)

theorem HCPolySupport.HighContrast.Response.affineCoeffSpace_inv_affineCoeffSpace {d : ℕ} (L : Mat d) (hL : IsUnit (Matrix.det L)) (a : CoeffSpace d) : affineCoeffSpace L⁻¹ ⋯ (affineCoeffSpace L hL a) = a

noncomputable def HCPolySupport.HighContrast.Response.affineCoeffSpaceEquiv {d : ℕ} (L : Mat d) (hL : IsUnit (Matrix.det L)) : CoeffSpace d ≃ᵐ CoeffSpace d

Affine transformation by L as a measurable equivalence of coefficient space, inverted by the transformation under L⁻¹.

Equations

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

theorem HCPolySupport.HighContrast.Response.integral_cutoffWeighted_affineResponseJ_eq_zero_of_stationarity {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) (E : CoeffSpace d ≃ᵐ CoeffSpace d) (hE : ∀ (z : Fin d → ℤ) (a : CoeffSpace d), translateCoeff z (E a) = E (translateCoeff z a)) (A : CoeffSpace d → Book.Ch02.TriadicCoeffFamily d) (hA : ∀ (a : CoeffSpace d) (Q : TriadicCube d), ((A a).coeffOn Q).toCoeffField = affineCoefficient q ⋯ ((E a).coeffOn (adaptedDomain hq t)).toCoeffField) (p r : Vec d) {phi : 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) (hphi : MeasureTheory.IntegrableOn phi (cubeSet (originCube d t)) MeasureTheory.volume) (hmean : cubeAverage (originCube d t) phi = 1) : ∫ (a : CoeffSpace d), descendantsAverage (originCube d t) j fun (R : TriadicCube d) => (1 - cubeAverage R phi) * Book.Ch02.responseJ (Book.Ch02.cubeDomain R) ((A a).coeffOn R) (matVecMul (matTranspose q) p) (matVecMul q⁻¹ r) ∂P = 0

A stationary affine family inherits the exact cutoff-weighted response cancellation from the unconditional triadic response congruence.