High-contrast homogenization: Provider.Quenched.TriadicDilationResponse

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

Coarse-response covariance under triadic dilation

The coarse response of a dilated coefficient sample on a reference cube is the response of the original sample on the corresponding larger cube. Passing this identity through the pushed-forward law gives exact covariance of the annealed block and its intrinsic contrast.

theorem HCPolySupport.HighContrast.coarseBlock_triadicDilation {d : ℕ} (n : ℕ) (Q : TriadicCube d) (a : CoeffSpace d) : coarseBlock (openCubeSet Q) (CoeffSpace.triadicDilation n a) = coarseBlock (openCubeSet (Book.Ch02.dilateCube (↑n) Q)) a

Pathwise coarse responses commute with triadic dilation of a cube.

theorem HCPolySupport.HighContrast.coarseBlock_standardCell_triadicDilation {d : ℕ} (n : ℕ) (k : ℤ) (w : Fin d → ℤ) (a : CoeffSpace d) : coarseBlock (standardCell d k w) (CoeffSpace.triadicDilation n a) = coarseBlock (standardCell d (↑n + k) w) a

On standard aligned cells, dilation shifts the integer generation and preserves the cell label.

theorem HCPolySupport.HighContrast.coarseBlock_centeredCube_triadicDilation {d : ℕ} (n : ℕ) (k : ℤ) (a : CoeffSpace d) : coarseBlock (centeredCube d k) (CoeffSpace.triadicDilation n a) = coarseBlock (centeredCube d (↑n + k)) a

On centered cubes, dilation shifts the integer generation.

theorem HCPolySupport.HighContrast.annealedBlock_triadicRebasedLaw {d : ℕ} (n : ℕ) (P : MeasureTheory.Measure (CoeffSpace d)) (k : ℤ) : annealedBlock (triadicRebasedLaw n P) (centeredCube d k) = annealedBlock P (centeredCube d (↑n + k))

Annealed blocks of the rebased law are the original annealed blocks at the shifted generation.

theorem HCPolySupport.HighContrast.annealedContrast_triadicRebasedLaw {d : ℕ} (n : ℕ) (P : MeasureTheory.Measure (CoeffSpace d)) (k : ℤ) : annealedContrast (triadicRebasedLaw n P) k = annealedContrast P (↑n + k)

The intrinsic annealed contrast has the same generation-shift covariance.