High-contrast homogenization: Provider.PortableHistory.MajorizationIndex

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

Splitting an aligned index along the subdivision of the coarse block

The proof of p.fixed.geometry.one.grid.propagation partitions the terminal cell ⋄_T^q into its 3^{d(T-b)} aligned scale-b cells and reads the part of the centered maximum e.scale.selection.fluctuation.history carried by scales at most b on each of them separately.

For that reading, an aligned scale-j center inside ⋄_T^q has to be exhibited as an aligned scale-j center inside one of the scale-b children. In the index coordinates of the adapted cubes this is division with a centered remainder: writing m = 3^{b-j}, every integer w is w' + m y with 2|w'| < m, and the admissibility bound 2|w| < 3^{T-j} = m 3^{T-b} then forces 2|y| < 3^{T-b}, both bounds being strict because the powers of three are odd. No center falls on a face of the subdivision: the centered remainder is exact.

The center of the child is an integral vector, so the response over the scale-j cell at w is the response over the scale-j cell at w' evaluated at the translated sample, which is the form the stationarity transport consumes.

Division with a centered remainder

theorem HCPolySupport.HighContrast.PortableHistory.exists_centered_split {m M c e : ℤ} (hm : 0 < m) (hc : m = 2 * c + 1) (he : M = 2 * e + 1) {w : ℤ} (hw : 2 * |w| < m * M) : ∃ (y : ℤ) (w' : ℤ), w = w' + m * y ∧ 2 * |w'| < m ∧ 2 * |y| < M

Centered division by an odd modulus. Every integer splits as w = w' + m y with |w'| below half of m, and an admissibility bound 2|w| < m M with M odd forces the strict bound 2|y| < M.

theorem HCPolySupport.HighContrast.PortableHistory.three_pow_toNat_split {j b T : ℤ} (hjb : j ≤ b) (hbT : b ≤ T) : 3 ^ (T - j).toNat = 3 ^ (b - j).toNat * 3 ^ (T - b).toNat

The three-power exponents of the two stages of the subdivision add up.

theorem HCPolySupport.HighContrast.PortableHistory.exists_index_split {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) {j b T : ℤ} (hjb : j ≤ b) (hbT : b ≤ T) {w : Fin d → ℤ} (hw : adaptedCellCenter q j w ∈ adaptedCell q T) : ∃ (y : Fin d → ℤ) (w' : Fin d → ℤ), adaptedCellCenter q b y ∈ adaptedCell q T ∧ adaptedCellCenter q j w' ∈ adaptedCell q b ∧ ∀ (i : Fin d), w i = w' i + 3 ^ (b - j).toNat * y i

Every aligned scale-j center of the terminal cell sits in a scale-b child. The index splits as w = w' + 3^{b-j} y, with the child index y admissible for the terminal cell and the residual index w' admissible for the centered scale-b cell.

theorem HCPolySupport.HighContrast.PortableHistory.adaptedCellCenter_split {d : ℕ} (q : Mat d) {j b : ℤ} (hjb : j ≤ b) {y w' w : Fin d → ℤ} (hw : ∀ (i : Fin d), w i = w' i + 3 ^ (b - j).toNat * y i) : adaptedCellCenter q j w = adaptedCellCenter q b y + adaptedCellCenter q j w'

The centers add along the split. The scale-j center at w is the scale-b center at y translated by the scale-j center at w'.

theorem HCPolySupport.HighContrast.PortableHistory.adaptedResponse_split {d : ℕ} (q : Mat d) {j b : ℤ} {y w' w v : Fin d → ℤ} (hw : adaptedCellCenter q j w = adaptedCellCenter q b y + adaptedCellCenter q j w') (hv : adaptedCellCenter q b y = fun (i : Fin d) => ↑(v i)) (a : CoeffSpace d) : adaptedResponse q j w a = adaptedResponse q j w' (translateCoeff v a)

The response at a split index is the response at the residual index of the translated sample. This is the translation invariance of the variational coarse block read along the subdivision.