High-contrast homogenization: Entry.Response.Direct.DescendantIndexStationarity

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

The descendant index decomposition and its stationarity reduction

The triadic index box enumerating the 3^{(m+1)d} aligned cells of one generation inside a coarser adapted cell splits every depth-(H+n) index into an outer index naming the depth-H cell containing it and an inner index naming its position there, a balanced-ternary grouping with its own bound and injectivity properties. Because the descendant sum of p.response.transfer cuts the terminal cell into generation-(s-n) aligned cells indexed exactly this way, stationarity of the coefficient law acts on the outer index alone: translating by the generation-s cell centre identifies a descendant cell's annealed coarse block with a fixed translate depending only on the inner index. A companion pair of lemmas telescopes the same descendant sum's weighted flat cell averages generation by generation down to depth H, the arithmetic the oscillation half of the cutoff-mean row sums against the source load.

The descendant telescoping of the cutoff cell weights

Refining the depth-m subdivision of the terminal cell into the depth-(m+1) subdivision turns the difference of the two weighted flat cell averages of the cutoff cell weights against the cell averages of a fixed integrable field into the flat average of the weight increment against the finer cell averages. Summing those increments over the generations telescopes the depth-N weighted flat average into the terminal depth-zero term plus the descendant sum that p.response.transfer bounds.

theorem HCPolySupport.HighContrast.Multiscale.avsum_weighted_volumeAverage_succ_sub {d : ℕ} [NeZero d] {q : Mat d} (hq : IsUnit q) (t : ℤ) (m : ℕ) (φ : Vec d → ℝ) {f : Vec d → ℝ} (hf : MeasureTheory.IntegrableOn f (adaptedCell q t) MeasureTheory.volume) : (↑(triadicIndexBox d (m + 1)).card)⁻¹ * ∑ W ∈ triadicIndexBox d (m + 1), (volumeAverage (adaptedCellAtCenter q (t - ↑(m + 1)) W) fun (x : Vec d) => φ x - 1) * volumeAverage (adaptedCellAtCenter q (t - ↑(m + 1)) W) f - (↑(triadicIndexBox d m).card)⁻¹ * ∑ w ∈ triadicIndexBox d m, (volumeAverage (adaptedCellAtCenter q (t - ↑m) w) fun (x : Vec d) => φ x - 1) * volumeAverage (adaptedCellAtCenter q (t - ↑m) w) f = (↑(triadicIndexBox d (m + 1)).card)⁻¹ * ∑ W ∈ triadicIndexBox d (m + 1), ((volumeAverage (adaptedCellAtCenter q (t - ↑(m + 1)) W) fun (x : Vec d) => φ x - 1) - volumeAverage (adaptedCellAtCenter q (t - ↑m) (Transport.gridParent W)) fun (x : Vec d) => φ x - 1) * volumeAverage (adaptedCellAtCenter q (t - ↑(m + 1)) W) f

The increment of the weighted flat cell average across one generation. Refining the depth-m subdivision into the depth-(m+1) subdivision turns the difference of the two weighted flat averages into the flat average of the weight increment against the finer cell averages.

theorem HCPolySupport.HighContrast.Multiscale.avsum_weighted_volumeAverage_eq_sum_range {d : ℕ} [NeZero d] {q : Mat d} (hq : IsUnit q) (t : ℤ) (N : ℕ) (φ : Vec d → ℝ) {f : Vec d → ℝ} (hf : MeasureTheory.IntegrableOn f (adaptedCell q t) MeasureTheory.volume) : (↑(triadicIndexBox d N).card)⁻¹ * ∑ W ∈ triadicIndexBox d N, (volumeAverage (adaptedCellAtCenter q (t - ↑N) W) fun (x : Vec d) => φ x - 1) * volumeAverage (adaptedCellAtCenter q (t - ↑N) W) f = (volumeAverage (adaptedCell q t) fun (x : Vec d) => φ x - 1) * volumeAverage (adaptedCell q t) f + ∑ m ∈ Finset.range N, (↑(triadicIndexBox d (m + 1)).card)⁻¹ * ∑ W ∈ triadicIndexBox d (m + 1), ((volumeAverage (adaptedCellAtCenter q (t - ↑(m + 1)) W) fun (x : Vec d) => φ x - 1) - volumeAverage (adaptedCellAtCenter q (t - ↑m) (Transport.gridParent W)) fun (x : Vec d) => φ x - 1) * volumeAverage (adaptedCellAtCenter q (t - ↑(m + 1)) W) f

The weighted flat cell average telescopes over the generations. The depth-N weighted flat average of the cutoff cell weights against the cell averages of f is the terminal term plus the sum of the generation increments. For a cutoff of the class IsResponseCutoff the terminal term vanishes, so the whole quantity is the descendant sum of p.response.transfer.

The oscillation decomposition of the cutoff-mean row

The oscillation half of the cutoff-mean row of p.response.transfer compares the (φ - 1)-weighted average of an integrable density f over the terminal cell with its depth-H cell part. Refining the subdivision generation by generation, that difference is the sum of the generation increments of the descendant sum, carried by the deeper cells, plus the defect of the farthest cell part. The telescoping identity at every depth produces both readings once it is subtracted from itself at the shifted depth.

theorem HCPolySupport.HighContrast.Multiscale.avsum_weighted_volumeAverage_add_sub_eq_sum_range {d : ℕ} [NeZero d] {q : Mat d} (hq : IsUnit q) (t : ℤ) (H N : ℕ) (φ : Vec d → ℝ) {f : Vec d → ℝ} (hf : MeasureTheory.IntegrableOn f (adaptedCell q t) MeasureTheory.volume) : (↑(triadicIndexBox d (H + N)).card)⁻¹ * ∑ W ∈ triadicIndexBox d (H + N), (volumeAverage (adaptedCellAtCenter q (t - ↑(H + N)) W) fun (x : Vec d) => φ x - 1) * volumeAverage (adaptedCellAtCenter q (t - ↑(H + N)) W) f - (↑(triadicIndexBox d H).card)⁻¹ * ∑ w ∈ triadicIndexBox d H, (volumeAverage (adaptedCellAtCenter q (t - ↑H) w) fun (x : Vec d) => φ x - 1) * volumeAverage (adaptedCellAtCenter q (t - ↑H) w) f = ∑ n ∈ Finset.range N, (↑(triadicIndexBox d (H + n + 1)).card)⁻¹ * ∑ W ∈ triadicIndexBox d (H + n + 1), ((volumeAverage (adaptedCellAtCenter q (t - ↑(H + n + 1)) W) fun (x : Vec d) => φ x - 1) - volumeAverage (adaptedCellAtCenter q (t - ↑(H + n)) (Transport.gridParent W)) fun (x : Vec d) => φ x - 1) * volumeAverage (adaptedCellAtCenter q (t - ↑(H + n + 1)) W) f

The shifted descendant telescoping. The difference between the depth-(H+N) and the depth-H weighted flat cell averages is the sum of the N generation increments below the scale-s cells, the depth-n increment being carried by the generation t - (H + n + 1).

theorem HCPolySupport.HighContrast.Multiscale.volumeAverage_sub_one_eq_cellPart_add_sum_range_add_rem {d : ℕ} [NeZero d] {q : Mat d} (hq : IsUnit q) (t : ℤ) (H N : ℕ) (φ : Vec d → ℝ) {f : Vec d → ℝ} (hf : MeasureTheory.IntegrableOn f (adaptedCell q t) MeasureTheory.volume) : (volumeAverage (adaptedCell q t) fun (x : Vec d) => (φ x - 1) * f x) = (↑(triadicIndexBox d H).card)⁻¹ * ∑ w ∈ triadicIndexBox d H, (volumeAverage (adaptedCellAtCenter q (t - ↑H) w) fun (x : Vec d) => φ x - 1) * volumeAverage (adaptedCellAtCenter q (t - ↑H) w) f + ∑ n ∈ Finset.range N, (↑(triadicIndexBox d (H + n + 1)).card)⁻¹ * ∑ W ∈ triadicIndexBox d (H + n + 1), ((volumeAverage (adaptedCellAtCenter q (t - ↑(H + n + 1)) W) fun (x : Vec d) => φ x - 1) - volumeAverage (adaptedCellAtCenter q (t - ↑(H + n)) (Transport.gridParent W)) fun (x : Vec d) => φ x - 1) * volumeAverage (adaptedCellAtCenter q (t - ↑(H + n + 1)) W) f + ((volumeAverage (adaptedCell q t) fun (x : Vec d) => (φ x - 1) * f x) - (↑(triadicIndexBox d (H + N)).card)⁻¹ * ∑ W ∈ triadicIndexBox d (H + N), (volumeAverage (adaptedCellAtCenter q (t - ↑(H + N)) W) fun (x : Vec d) => φ x - 1) * volumeAverage (adaptedCellAtCenter q (t - ↑(H + N)) W) f)

The oscillation decomposition of the cutoff-mean row at every refinement depth. The (φ-1)-weighted average of f over the terminal cell is its depth-H cell part, plus the first N generation increments of the descendant sum of p.response.transfer, plus a remainder which is the defect of the depth-(H+N) cell part.

Grouping the triadic index box at 3 ^ n

triadicIndexBox d m indexes the 3 ^ (m * d) aligned cells of generation t - m inside the adapted cell of generation t. Writing a generation gap as H + n, every depth-(H + n) index W splits uniquely as W = 3 ^ n * w + z, with w the outer index of the depth-H cell containing the cell and z the inner index of the cell inside it. This is balanced ternary with the digits grouped at 3 ^ n. It is what lets the descendant sum of p.response.transfer read the annealed head of the source load: the 3 ^ ((H + n) * d) descendants of the terminal cell at generation s - n are exactly 3 ^ (H * d) translated copies of the 3 ^ (n * d) descendants of one scale-s cell.

The proof needs no explicit inverse: the grouped-digit map is injective and the two finsets have the same cardinality, so its image is everything.

def HCPolySupport.HighContrast.Multiscale.triadicIndexBound (m : ℕ) : ℕ

triadicIndexBound m = (3 ^ m - 1) / 2 is the radius of the depth-m index box triadicIndexBox d m, i.e. the box is the integer interval [-b m, b m] in every coordinate.

Equations

• HCPolySupport.HighContrast.Multiscale.triadicIndexBound m = (3 ^ m - 1) / 2

theorem HCPolySupport.HighContrast.Multiscale.mem_triadicIndexBox_add_of_mem {d H n : ℕ} {w z : Fin d → ℤ} (hw : w ∈ triadicIndexBox d H) (hz : z ∈ triadicIndexBox d n) : (fun (i : Fin d) => 3 ^ n * w i + z i) ∈ triadicIndexBox d (H + n)

The grouped-digit index is in the box. If the outer index w lies in the box of depth H and the inner index z in the box of depth n, then 3^n w + z lies in the box of depth H + n.

theorem HCPolySupport.HighContrast.Multiscale.triadicIndexBox_add_injOn {d H n : ℕ} {w z w' z' : Fin d → ℤ} (hz : z ∈ triadicIndexBox d n) (hz' : z' ∈ triadicIndexBox d n) (h : (fun (i : Fin d) => 3 ^ n * w i + z i) = fun (i : Fin d) => 3 ^ n * w' i + z' i) : w = w' ∧ z = z'

The grouped-digit map is injective. Two pairs of an outer and an inner index that give the same grouped index are equal: the inner digits span less than one outer step.

theorem HCPolySupport.HighContrast.Multiscale.sum_triadicIndexBox_add {d : ℕ} (H n : ℕ) (F : (Fin d → ℤ) → ℝ) : ∑ W ∈ triadicIndexBox d (H + n), F W = ∑ w ∈ triadicIndexBox d H, ∑ z ∈ triadicIndexBox d n, F fun (i : Fin d) => 3 ^ n * w i + z i

The index box of depth H + n is the grouped product of the boxes of depths H and n. Summing a function over the depth-(H+n) box is summing it over the outer box of the depth-H cells and, inside each, over the inner box of the depth-n descendants.

The annealed block of a descendant cell depends only on its inner index

In the descendant sum of p.response.transfer the terminal cell is cut into the 3^{(H+n)d} aligned cells of generation s - n, indexed by 3^n w + z with w the index of the scale-s cell containing the descendant and z the index of the descendant inside that cell. Stationarity acts on the outer index alone: the generation-s translation 3^s q w is an integer vector once s ≥ j_*, the law is invariant under integer translations, and the recentring a_- = a - g, a_+ = aᵀ + g adds a constant matrix field, which commutes with translation. Hence the annealed block of the descendant cell does not depend on w, only on the inner index z.

This is the descendant form of the landed annealedBlockOf_adaptedCellAtCenter_respCoeffMinus_eq, whose case n = 0 recovers that statement.

theorem HCPolySupport.HighContrast.Multiscale.annealedBlockOf_descendant_respCoeffMinus_eq {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (hstat : IsStationaryLaw P) (jStar : ℕ) (m : Mat d) (F : BlockMat d) (j : ℤ) (hj : ↑jStar ≤ j) (n : ℕ) (w z : Fin d → ℤ) (hmeas : ∀ (i k : Fin d), MeasureTheory.AEStronglyMeasurable (fun (a : CoeffSpace d) => (coarseBlockMatrix (adaptedCellAtCenter (Geometry.explicitRoundedGrid jStar m) (j - ↑n) z) (respCoeffMinus F a)).upperLeft i k) P) (hmeas' : ∀ (i k : Fin d), MeasureTheory.AEStronglyMeasurable (fun (a : CoeffSpace d) => (coarseBlockMatrix (adaptedCellAtCenter (Geometry.explicitRoundedGrid jStar m) (j - ↑n) z) (respCoeffMinus F a)).lowerRight i k) P) : (annealedBlockOf P (adaptedCellAtCenter (Geometry.explicitRoundedGrid jStar m) (j - ↑n) fun (i : Fin d) => 3 ^ n * w i + z i) (respCoeffMinus F)).upperLeft = (annealedBlockOf P (adaptedCellAtCenter (Geometry.explicitRoundedGrid jStar m) (j - ↑n) z) (respCoeffMinus F)).upperLeft ∧ (annealedBlockOf P (adaptedCellAtCenter (Geometry.explicitRoundedGrid jStar m) (j - ↑n) fun (i : Fin d) => 3 ^ n * w i + z i) (respCoeffMinus F)).lowerRight = (annealedBlockOf P (adaptedCellAtCenter (Geometry.explicitRoundedGrid jStar m) (j - ↑n) z) (respCoeffMinus F)).lowerRight

The annealed block of a descendant cell is independent of the scale-j cell containing it, minus sign. For a stationary law and a scale j >= j_*, the annealed block of the generation-(j - n) aligned cell at the grouped index 3^n w + z is the annealed block of the generation-(j - n) aligned cell at the inner index z.

theorem HCPolySupport.HighContrast.Multiscale.annealedBlockOf_descendant_respCoeffPlus_eq {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (hstat : IsStationaryLaw P) (jStar : ℕ) (m : Mat d) (F : BlockMat d) (j : ℤ) (hj : ↑jStar ≤ j) (n : ℕ) (w z : Fin d → ℤ) (hmeas : ∀ (i k : Fin d), MeasureTheory.AEStronglyMeasurable (fun (a : CoeffSpace d) => (coarseBlockMatrix (adaptedCellAtCenter (Geometry.explicitRoundedGrid jStar m) (j - ↑n) z) (respCoeffPlus F a)).upperLeft i k) P) (hmeas' : ∀ (i k : Fin d), MeasureTheory.AEStronglyMeasurable (fun (a : CoeffSpace d) => (coarseBlockMatrix (adaptedCellAtCenter (Geometry.explicitRoundedGrid jStar m) (j - ↑n) z) (respCoeffPlus F a)).lowerRight i k) P) : (annealedBlockOf P (adaptedCellAtCenter (Geometry.explicitRoundedGrid jStar m) (j - ↑n) fun (i : Fin d) => 3 ^ n * w i + z i) (respCoeffPlus F)).upperLeft = (annealedBlockOf P (adaptedCellAtCenter (Geometry.explicitRoundedGrid jStar m) (j - ↑n) z) (respCoeffPlus F)).upperLeft ∧ (annealedBlockOf P (adaptedCellAtCenter (Geometry.explicitRoundedGrid jStar m) (j - ↑n) fun (i : Fin d) => 3 ^ n * w i + z i) (respCoeffPlus F)).lowerRight = (annealedBlockOf P (adaptedCellAtCenter (Geometry.explicitRoundedGrid jStar m) (j - ↑n) z) (respCoeffPlus F)).lowerRight

The annealed block of a descendant cell is independent of the scale-j cell containing it, plus sign. The adjoint twin of annealedBlockOf_descendant_respCoeffMinus_eq, for the recentred family a_+ = a^t + g.