High-contrast homogenization: Entry.Annealed.TransportDriftAlgebra

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

Abel summation and the drift-weight algebra of the two-grid transport

The finite summation-by-parts identity on integer intervals, the exact base-three difference of the exponential drift weights, and the resulting total-mass-one identity those weights satisfy. The same algebra is applied to the actual determinant drift and the actual normalized means, separating the terminal boundary trace from the interior geometric convolution of trace excesses, and is quantified into the error, sum, bulk, boundary, source and scalar-assembly bounds that supply the drift term of p.two.grid.transport.

theorem HCPolySupport.HighContrast.Annealed.transport_abel_identity (w f : ℤ → ℝ) (J t : ℤ) (hJt : J < t) : ∑ r ∈ Finset.Icc (J + 1) t, w r * (f (r - 1) - f r) = w (J + 1) * f J + ∑ j ∈ Finset.Icc (J + 1) (t - 1), (w (j + 1) - w j) * f j - w t * f t

Finite summation by parts, including the one-increment interval.

theorem HCPolySupport.HighContrast.Annealed.transport_abel_weight (a : ℝ) (t j : ℤ) : 3 ^ (-a * (↑t - (↑j + 1))) - 3 ^ (-a * (↑t - ↑j)) = (1 - 3 ^ (-a)) * 3 ^ (-a * (↑t - ↑j - 1))

The printed drift weight difference, with its fixed one-generation shift.

theorem HCPolySupport.HighContrast.Annealed.transport_abel_mass (a : ℝ) (J t : ℤ) (hJt : J < t) : 3 ^ (-a * (↑t - ↑J - 1)) + (1 - 3 ^ (-a)) * ∑ j ∈ Finset.Icc (J + 1) (t - 1), 3 ^ (-a * (↑t - ↑j - 1)) = 1

The Abel coefficients have total mass one, even when the interior sum is empty.

theorem HCPolySupport.HighContrast.Annealed.transport_trace_sub {d : ℕ} (A B : BlockMat d) : blockTrace (blockSub A B) = blockTrace A - blockTrace B

The trace of a block difference is the difference of its traces.

theorem HCPolySupport.HighContrast.Annealed.transport_determinantDrift_abel {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (γ : ℝ) (q : Mat d) (jStar : ℕ) (t : ℤ) (hJt : ↑jStar < t) (ht : Matrix.PosDef (toFullBlockMat (adaptedMean P q t))) : determinantDrift P γ q jStar t = 3 ^ (-((1 - γ) / 8) * (↑t - ↑jStar - 1)) * blockTrace (blockSub (relMean P q (↑jStar) t) (Book.Ch02.blockIdentity d)) + (1 - 3 ^ (-((1 - γ) / 8))) * ∑ j ∈ Finset.Icc (↑jStar + 1) (t - 1), 3 ^ (-((1 - γ) / 8) * (↑t - ↑j - 1)) * blockTrace (blockSub (relMean P q j t) (Book.Ch02.blockIdentity d))

Abel summation for the actual determinant drift and actual normalized means.

theorem HCPolySupport.HighContrast.Annealed.transport_abel_error (a : ℝ) (ha : 0 ≤ a) (J t : ℤ) (hJt : J < t) (f g : ℤ → ℝ) (D : ℝ) (hfg : ∀ j ∈ Finset.Icc J (t - 1), f j ≤ g j + D) : 3 ^ (-a * (↑t - ↑J - 1)) * f J + (1 - 3 ^ (-a)) * ∑ j ∈ Finset.Icc (J + 1) (t - 1), 3 ^ (-a * (↑t - ↑j - 1)) * f j ≤ 3 ^ (-a * (↑t - ↑J - 1)) * g J + (1 - 3 ^ (-a)) * ∑ j ∈ Finset.Icc (J + 1) (t - 1), 3 ^ (-a * (↑t - ↑j - 1)) * g j + D

A mass-one nonnegative Abel combination accumulates a uniform error once.

theorem HCPolySupport.HighContrast.Annealed.transport_abel_sum_bound (a : ℝ) (ha : 0 < a) (J m : ℤ) (hJm : J < m) (f : ℤ → ℝ) (hf : ∀ j ∈ Finset.Icc J (m - 1), 0 ≤ f j) (D : ℝ) (hD : 3 ^ (-a * (↑m - ↑J - 1)) * f J + (1 - 3 ^ (-a)) * ∑ j ∈ Finset.Icc (J + 1) (m - 1), 3 ^ (-a * (↑m - ↑j - 1)) * f j = D) : ∑ j ∈ Finset.Icc J (m - 1), 3 ^ (-a * (↑m - ↑j - 1)) * f j ≤ 1 / (1 - 3 ^ (-a)) * D

The weighted sum of all nonnegative trace excesses is controlled by its Abel expression.

theorem HCPolySupport.HighContrast.Annealed.transport_drift_bulk_weights (a : ℝ) (J n : ℤ) (L : ℕ) (f : ℤ → ℝ) (hf : ∀ r ∈ Finset.Icc J (n + 2 * ↑L - 1), 0 ≤ f r) : ∑ j ∈ Finset.Icc (J + ↑L) (n + ↑L - 1), 3 ^ (-a * (↑n + ↑L - ↑j - 1)) * f (j - ↑L) ≤ 3 ^ (2 * a * ↑L) * ∑ r ∈ Finset.Icc J (n + 2 * ↑L - 1), 3 ^ (-a * (↑n + 2 * ↑L - ↑r - 1)) * f r

Translating the bulk generation shifts its weight by exactly two bridge lengths.

theorem HCPolySupport.HighContrast.Annealed.transport_drift_boundary_weights (a : ℝ) (ha : a < 1) (J n : ℤ) (L : ℕ) (f : ℤ → ℝ) (hf : ∀ r ∈ Finset.Icc J (n + 2 * ↑L - 1), 0 ≤ f r) : ∑ j ∈ Finset.Icc (J + ↑L) (n + ↑L - 1), 3 ^ (-a * (↑n + ↑L - ↑j - 1)) * ∑ r ∈ Finset.Icc J (j - ↑L - 1), 3 ^ (↑r - ↑j) * f r ≤ 3 ^ (a * ↑L) / (1 - 3 ^ (-(1 - a))) * ∑ r ∈ Finset.Icc J (n + 2 * ↑L - 1), 3 ^ (-a * (↑n + 2 * ↑L - ↑r - 1)) * f r

The boundary trace sum is a geometric convolution normalized at the old terminal scale.

theorem HCPolySupport.HighContrast.Annealed.transport_drift_trace_nonneg (d : ℕ) (hd : 2 ≤ d) (P : MeasureTheory.Measure (CoeffSpace d)) [MeasureTheory.IsProbabilityMeasure P] (γ : ℝ) (E : BlockMat d) (Ψ : ℝ → ℝ) (K : ℝ) (S : CoeffSpace d → ℝ) (hstat : IsStationaryLaw P) (hdag : CoarseEllipticityDagger P γ E Ψ K S) (jStar : ℕ) (hj : 2 * d ≤ 3 ^ jStar) (m : Mat d) (hm : Matrix.PosDef m) (r t : ℤ) (hJr : ↑jStar ≤ r) (hrt : r ≤ t) : 0 ≤ blockTrace (blockSub (relMean P (Geometry.explicitRoundedGrid jStar m) r t) (Book.Ch02.blockIdentity d))

Trace excesses of actual normalized means are nonnegative throughout the ordered range.

theorem HCPolySupport.HighContrast.Annealed.transport_normalized_trace_sum {d : ℕ} (A : ℤ → BlockMat d) (F : BlockMat d) (hF : Matrix.PosDef (toFullBlockMat F)) (I : Finset ℤ) (b : ℤ) (w : ℤ → ℝ) (C D : ℝ) : blockTrace (normalizedBlock (ofFullBlockMat (toFullBlockMat (A b) + C • ∑ r ∈ I, w r • toFullBlockMat (A r) + D • toFullBlockMat F)) F) = blockTrace (normalizedBlock (A b) F) + C * ∑ r ∈ I, w r * blockTrace (normalizedBlock (A r) F) + D * (2 * ↑d)

Linearity of the normalized trace keeps the identity contribution explicit.

theorem HCPolySupport.HighContrast.Annealed.transport_drift_trace_comparison {d : ℕ} (A : ℤ → BlockMat d) (H F : BlockMat d) (hA : ∀ (r : ℤ), Matrix.PosDef (toFullBlockMat (A r))) (hH : Matrix.PosDef (toFullBlockMat H)) (hF : Matrix.PosDef (toFullBlockMat F)) (I : Finset ℤ) (b : ℤ) (w : ℤ → ℝ) (hw : ∀ (r : ℤ), 0 ≤ w r) (C D : ℝ) (hC : 0 ≤ C) (hD : 0 ≤ D) (hbound : BlockMatLoewnerLE H (ofFullBlockMat (toFullBlockMat (A b) + C • ∑ r ∈ I, w r • toFullBlockMat (A r) + D • toFullBlockMat F))) : blockTrace (blockSub (normalizedBlock H F) (Book.Ch02.blockIdentity d)) ≤ blockTrace (blockSub (normalizedBlock (A b) F) (Book.Ch02.blockIdentity d)) + C * ∑ r ∈ I, w r * blockTrace (blockSub (normalizedBlock (A r) F) (Book.Ch02.blockIdentity d)) + 2 * ↑d * C * ∑ r ∈ I, w r + 2 * ↑d * D

Taking a normalized trace of the Whitney matrix bound separates excess and identity.

theorem HCPolySupport.HighContrast.Annealed.transport_drift_identity_row (J j : ℤ) (L : ℕ) : ∑ r ∈ Finset.Icc J (j - ↑L - 1), 3 ^ (↑r - ↑j) ≤ 1 / (1 - 3 ^ (-1)) * 3 ^ (-↑L)

Scalar geometric bound for the boundary identity row, including an empty row.

theorem HCPolySupport.HighContrast.Annealed.transport_abel_le_sum (a : ℝ) (J t : ℤ) (hJt : J < t) (f : ℤ → ℝ) (hf : ∀ j ∈ Finset.Icc J (t - 1), 0 ≤ f j) : 3 ^ (-a * (↑t - ↑J - 1)) * f J + (1 - 3 ^ (-a)) * ∑ j ∈ Finset.Icc (J + 1) (t - 1), 3 ^ (-a * (↑t - ↑j - 1)) * f j ≤ ∑ j ∈ Finset.Icc J (t - 1), 3 ^ (-a * (↑t - ↑j - 1)) * f j

Nonnegative Abel coefficients are bounded by the corresponding full geometric sum.

theorem HCPolySupport.HighContrast.Annealed.transport_drift_source_weight (a b : ℝ) (ha : 0 ≤ a) (hab : a ≤ b) (J n j : ℤ) (hj : J ≤ j) (L : ℕ) (hL : 1 ≤ L) : (3 ^ (-a * (↑n + ↑L - ↑j - 1)) * if j < J + ↑L then 1 else 3 ^ (-b * (↑j - ↑J))) ≤ 3 ^ (-a * (↑n - ↑J))

Each early-source or late-source weight is paid by the printed source decay.

theorem HCPolySupport.HighContrast.Annealed.transport_drift_source_weights (a b : ℝ) (ha : 0 ≤ a) (hab : a ≤ b) (J n : ℤ) (hn : J ≤ n) (L : ℕ) (hL : 1 ≤ L) : (∑ j ∈ Finset.Icc J (n + ↑L - 1), 3 ^ (-a * (↑n + ↑L - ↑j - 1)) * if j < J + ↑L then 1 else 3 ^ (-b * (↑j - ↑J))) ≤ (↑n + ↑L - ↑J) * 3 ^ (-a * (↑n - ↑J))

Summing the common source weight retains the printed linear factor in the scale gap.

theorem HCPolySupport.HighContrast.Annealed.transport_drift_scalar_assembly (a b : ℝ) (ha : 0 < a) (ha1 : a < 1) (hab : a ≤ b) (J n : ℤ) (hn : J ≤ n) (L : ℕ) (hL : 1 ≤ L) (f g : ℤ → ℝ) (hf : ∀ r ∈ Finset.Icc J (n + 2 * ↑L - 1), 0 ≤ f r) (A Cb Y E : ℝ) (hA : 0 ≤ A) (hCb : 0 ≤ Cb) (hY : 0 ≤ Y) (hpoint : ∀ j ∈ Finset.Icc J (n + ↑L - 1), g j ≤ ((A * if j < J + ↑L then 0 else f (j - ↑L) + Cb * ∑ r ∈ Finset.Icc J (j - ↑L - 1), 3 ^ (↑r - ↑j) * f r) + Y * if j < J + ↑L then 1 else 3 ^ (-b * (↑j - ↑J))) + E) : 3 ^ (-a * (↑n + ↑L - ↑J - 1)) * g J + (1 - 3 ^ (-a)) * ∑ j ∈ Finset.Icc (J + 1) (n + ↑L - 1), 3 ^ (-a * (↑n + ↑L - ↑j - 1)) * g j ≤ A * 3 ^ (2 * a * ↑L) * (1 + Cb / (1 - 3 ^ (-(1 - a)))) * ∑ r ∈ Finset.Icc J (n + 2 * ↑L - 1), 3 ^ (-a * (↑n + 2 * ↑L - ↑r - 1)) * f r + Y * (↑n + ↑L - ↑J) * 3 ^ (-a * (↑n - ↑J)) + E

Assemble the Abel terms after the uniform comparison and identity errors have been separated.

theorem HCPolySupport.HighContrast.Annealed.transport_normalized_trace_scalar_bound {d : ℕ} (A F : BlockMat d) (hA : Matrix.PosSemidef (toFullBlockMat A)) (hF : Matrix.PosDef (toFullBlockMat F)) (M : ℝ) (hM : 0 ≤ M) (hbound : BlockMatLoewnerLE A (blockScale M F)) : blockTrace (blockSub (normalizedBlock A F) (Book.Ch02.blockIdentity d)) ≤ 2 * ↑d * M

A source matrix upper bound controls its normalized trace excess.