High-contrast homogenization: Provider.Transport.DiscreteConvolution

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

The discrete convolutions of the grid transport

The transport pays every source scale into every target scale, and the two resulting sums are discrete convolutions against a geometric kernel. This file proves them, together with the one combinatorial fact they need.

The workhorse is a geometric bound with no interval hypothesis: an arbitrary finite set of integers on one side of a threshold carries at most the full geometric weight measured from that threshold. The transport needs exactly this generality, because the target scales that share a given auxiliary depth do not form an interval.

Three displayed convolutions follow. The bulk convolution e.two.grid.bulk.mean is an identity: shifting a source scale down by the auxiliary depth converts the row weight at the new terminal scale into the row weight at the old one, at the exact cost 3^{a(ℓ₀+λ)}, which the bound λ ≤ ℓ₀ turns into the buffer factor 3^{2aℓ₀}. The boundary convolution e.two.grid.boundary.mean sums the conservative row 3^{-(1-g)(j-r)} against the same weights; the series converges precisely because the derived exponent is below 1 - g, and its exact value 3^{-(1-g-a)λ}(1 - 3^{-(1-g-a)})^{-1} is exhibited rather than named. The bridge error acquires neither buffer factor: both of its sums are bare geometric series, the first because Qρ_max - d = Qg + a is positive and the second because a is.

The combinatorial fact is the multiplicity of the auxiliary depth. The depth takes one of two values, so the map carrying a target scale to its bulk source scale is at most two-to-one, and an adaptive bulk sum costs a factor two against the sum over source scales.

The geometric weight of an arbitrary finite set of scales

theorem HCPolySupport.HighContrast.Transport.sum_geom_above_le {c : ℝ} (hc : 0 < c) (lo : ℤ) (s : Finset ℤ) (hs : ∀ m ∈ s, lo ≤ m) : ∑ m ∈ s, 3 ^ (-c * (↑m - ↑lo)) ≤ 1 / (1 - 3 ^ (-c))

The geometric weight above a threshold. Any finite set of integers at or above lo, weighted by the geometric decay measured from lo, carries at most the total weight (1 - 3^{-c})^{-1} of the full series.

theorem HCPolySupport.HighContrast.Transport.sum_geom_below_le {c : ℝ} (hc : 0 < c) (hi : ℤ) (s : Finset ℤ) (hs : ∀ j ∈ s, j ≤ hi) : ∑ j ∈ s, 3 ^ (-c * (↑hi - ↑j)) ≤ 1 / (1 - 3 ^ (-c))

The geometric weight below a threshold. The reflected form of sum_geom_above_le: any finite set of integers at or below hi, weighted by the geometric decay measured from hi, carries at most the total weight of the full series.

The bridge error

theorem HCPolySupport.HighContrast.Transport.bridge_error_nonlinear {a etaX : ℝ} (ha : 0 < a) (heta : 0 ≤ etaX) (jStar n : ℤ) : ∑ j ∈ Finset.Ico jStar n, 3 ^ (-a * (↑n - 1 - ↑j)) * etaX ≤ 1 / (1 - 3 ^ (-a)) * etaX

The bridge error of the nonlinear history. Here the weight is the nonlinear row weight itself, and positivity of the derived exponent already sums it.

The bulk convolution

theorem HCPolySupport.HighContrast.Transport.bulk_convolution_eq {a : ℝ} (l0 lam n t j : ℝ) (ht : t = n + l0) : 3 ^ (-a * (n - 1 - j)) = 3 ^ (a * (l0 + lam)) * 3 ^ (-a * (t - 1 - (j - lam)))

e.two.grid.bulk.mean, the exact ratio. Shifting the source scale down by the auxiliary depth converts the row weight at the new terminal scale into the row weight at the old one, at the cost 3^{a(ℓ₀+λ)}.

theorem HCPolySupport.HighContrast.Transport.bulk_convolution_le {a : ℝ} (ha : 0 ≤ a) {l0 lam n t j : ℝ} (ht : t = n + l0) (hlam : lam ≤ l0) : 3 ^ (-a * (n - 1 - j)) ≤ 3 ^ (2 * a * l0) * 3 ^ (-a * (t - 1 - (j - lam)))

e.two.grid.bulk.mean. The auxiliary depth never exceeds the buffer, so the exact ratio is at most 3^{2aℓ₀}, with equality on the deep branch.

The boundary convolution

theorem HCPolySupport.HighContrast.Transport.boundary_convolution {a g : ℝ} (hahi : a < 1 - g) {l0 n t : ℤ} (ht : t = n + l0) (lam r : ℤ) (s : Finset ℤ) (hs : ∀ j ∈ s, r + lam ≤ j) : ∑ j ∈ s, 3 ^ (-a * (↑n - 1 - ↑j)) * 3 ^ (-(1 - g) * (↑j - ↑r)) ≤ 3 ^ (a * ↑l0) * (3 ^ (-(1 - g - a) * ↑lam) / (1 - 3 ^ (-(1 - g - a)))) * 3 ^ (-a * (↑t - 1 - ↑r))

e.two.grid.boundary.mean. Summing the conservative boundary row 3^{-(1-g)(j-r)} against the nonlinear row weights of the new terminal scale, over any set of target scales at depth at least λ above the source, costs one buffer factor 3^{aℓ₀} and the geometric series of ratio 3^{-(1-g-a)} started at λ. The series converges exactly because the derived exponent is below 1 - g.

The multiplicity of the auxiliary depth

theorem HCPolySupport.HighContrast.Transport.one_le_depth_and_le {l0 : ℤ} (hl0 : 1 ≤ l0) {lam : ℤ → ℤ} (hlam : ∀ (j : ℤ), lam j = 1 ∨ lam j = l0) (j : ℤ) : 1 ≤ lam j ∧ lam j ≤ l0

The adaptive depth of the Whitney filling. The deterministic auxiliary depth is either one or the full buffer, hence lies between one and the buffer.

theorem HCPolySupport.HighContrast.Transport.card_filter_sub_depth_le_two {l0 : ℤ} (lam : ℤ → ℤ) (hlam : ∀ (j : ℤ), lam j = 1 ∨ lam j = l0) (s : Finset ℤ) (m : ℤ) : {j ∈ s | j - lam j = m}.card ≤ 2

The auxiliary depth is at most two-to-one. The deterministic depth takes one of two values, so at most two target scales are carried to a given bulk source scale.

theorem HCPolySupport.HighContrast.Transport.sum_comp_sub_depth_le {l0 : ℤ} (lam : ℤ → ℤ) (hlam : ∀ (j : ℤ), lam j = 1 ∨ lam j = l0) (s t : Finset ℤ) (F : ℤ → ℝ) (hF : ∀ (m : ℤ), 0 ≤ F m) (hmem : ∀ j ∈ s, j - lam j ∈ t) : ∑ j ∈ s, F (j - lam j) ≤ 2 * ∑ m ∈ t, F m

The adaptive bulk sum costs a factor two. A sum over target scales of a nonnegative quantity read at the bulk source scale is at most twice the sum over source scales, by the multiplicity of the auxiliary depth.