High-contrast homogenization: Provider.Response.WeakNormGeometric

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

The geometric sum of the scale weights

Both scale sums of the weak-norm estimate are closed by the geometric sum over scales,

Σ_{k = -∞}^{t} 3^{(s - ρ/2)(k - t)} ≤ C/(2s - ρ),

used at the exponent s - ρ/2 ∈ (0, 1) on the bad event and at the exponent s on the old scales, where the printed right side C/(2s-ρ) is 2/(s - ρ/2) for C = 4. Reindexed by j = t - k, the sum is the ordinary geometric series in the ratio 3^{-a}, and the bound comes from the convexity estimate 3^{-a} ≤ 1 - a/2 on 0 < a ≤ 1: since log 3 ≥ 1,

3^{-a} ≤ e^{-a} ≤ (1 + a)^{-1} ≤ 1 - a/2,

the last step because a(1-a) ≥ 0. The tail form is the same bound after the common factor 3^{-aH} of the old scales k < t - H is taken out.

Nothing here is specific to the seminorm; the module is placed beside it because the weights it sums are the weights of the scale-average seminorm.

The geometric sum of the scale weights

theorem HCPolySupport.HighContrast.Response.rpow_three_neg_natCast (a : ℝ) (j : ℕ) : 3 ^ (-(a * ↑j)) = (3 ^ (-a)) ^ j

The scale weight at the scale k = t - j is the j-th power of the ratio 3^{-a}, which is what makes the printed scale sum geometric.

theorem HCPolySupport.HighContrast.Response.rpow_three_neg_le {a : ℝ} (ha : 0 < a) (ha1 : a ≤ 1) : 3 ^ (-a) ≤ 1 - a / 2

The base of the scale weights is below 1 - a/2.

theorem HCPolySupport.HighContrast.Response.tsum_rpow_three_neg_le {a : ℝ} (ha : 0 < a) (ha1 : a ≤ 1) : ∑' (j : ℕ), 3 ^ (-(a * ↑j)) ≤ 2 / a

The geometric sum of the scale weights: Σ_{k ≤ t}3^{a(k-t)} ≤ 2/a for 0 < a ≤ 1, applied at a = s and at a = s - ρ/2, where the printed bound C/(2s-ρ) is 4/(2s-ρ) = 2/(s-ρ/2).

theorem HCPolySupport.HighContrast.Response.tsum_rpow_three_neg_shift_le {a : ℝ} (ha : 0 < a) (ha1 : a ≤ 1) (n : ℕ) : ∑' (j : ℕ), 3 ^ (-(a * (↑j + ↑n))) ≤ 3 ^ (-(a * ↑n)) * (2 / a)

The tail of the geometric sum, the form in which the contribution of the old scales k < t - H is summed.

theorem HCPolySupport.HighContrast.Response.summable_rpow_three_neg {a : ℝ} (ha : 0 < a) (ha1 : a ≤ 1) : Summable fun (j : ℕ) => 3 ^ (-(a * ↑j))

The scale weights form a summable family, so the printed scale sum has a real value and the seminorm's majorants are finite.