Coarse-graining support:

Support.Deterministic.ConstantCoefficientDirichletBesov.DiscreteConvolution

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

Finite lower-triangular convolution estimates

This file contains the purely discrete summation step used by the hard standard-to-overlapping positive comparison. The analytic estimates produce a lower-triangular convolution in the depth variables; once the row and column geometric weights are bounded, the following finite Cauchy-Schwarz argument turns it into an l² estimate.

theorem HCPolySupport.lowerTriangularConvolution_sq_sum_le (N : ℕ) (K : ℝ) (w : ℕ → ℕ → ℝ) (a : ℕ → ℝ) (hK_nonneg : 0 ≤ K) (hw_nonneg : ∀ (j m : ℕ), 0 ≤ w j m) (hrow : ∀ j ∈ Finset.range (N + 1), ∑ m ∈ Finset.range j, w j m ≤ K) (hcol : ∀ m ∈ Finset.range (N + 1), ∑ j ∈ Finset.range (N + 1) with m < j, w j m ≤ K) : ∑ j ∈ Finset.range (N + 1), (∑ m ∈ Finset.range j, w j m * a m) ^ 2 ≤ K ^ 2 * ∑ m ∈ Finset.range (N + 1), a m ^ 2

theorem HCPolySupport.sum_range_geometric_pow_sub_le_inv {r : ℝ} (hr_nonneg : 0 ≤ r) (hr_lt_one : r < 1) (j : ℕ) : ∑ m ∈ Finset.range j, r ^ (j - m) ≤ (1 - r)⁻¹

Row sums for the lower-triangular geometric kernel. The exponent starts at 1 because m < j, but we bound it by the full geometric series starting at 0.

theorem HCPolySupport.sum_filter_geometric_pow_sub_le_inv {r : ℝ} (hr_nonneg : 0 ≤ r) (hr_lt_one : r < 1) (N m : ℕ) : ∑ j ∈ Finset.range (N + 1) with m < j, r ^ (j - m) ≤ (1 - r)⁻¹

Column sums for the lower-triangular geometric kernel.

theorem HCPolySupport.lowerTriangularGeometricConvolution_sq_sum_le (N : ℕ) {r : ℝ} (a : ℕ → ℝ) (hr_nonneg : 0 ≤ r) (hr_lt_one : r < 1) : ∑ j ∈ Finset.range (N + 1), (∑ m ∈ Finset.range j, r ^ (j - m) * a m) ^ 2 ≤ (1 - r)⁻¹ ^ 2 * ∑ m ∈ Finset.range (N + 1), a m ^ 2

Finite l² boundedness of the lower-triangular geometric convolution.

theorem HCPolySupport.sq_sum_le_of_le_add_geometric_convolution_sq (N : ℕ) {A B r : ℝ} (x a : ℕ → ℝ) (hB_nonneg : 0 ≤ B) (hr_nonneg : 0 ≤ r) (hr_lt_one : r < 1) (hdepth : ∀ j ∈ Finset.range (N + 1), x j ^ 2 ≤ A * a j ^ 2 + B * (∑ m ∈ Finset.range j, r ^ (j - m) * a m) ^ 2) : ∑ j ∈ Finset.range (N + 1), x j ^ 2 ≤ (A + B * (1 - r)⁻¹ ^ 2) * ∑ m ∈ Finset.range (N + 1), a m ^ 2

Finite-depth summation of a one-depth estimate with a geometric lower-triangular tail.