High-contrast homogenization: Provider.Response.ProfileRowAlignedSum #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
The finite geometric row above the alignment scale #
This is the scalar sum exchange behind
e.bridge.boundary.sum. The response exponent is fixed at
3/2, while the terminal increment row may use any nonnegative exponent
strictly below it.
theorem
HCPolySupport.HighContrast.Response.profileRow_weighted_tail_le
{rhoDr : ℝ}
(hrho : rhoDr < 3 / 2)
{jStar s : ℤ}
(x : ℤ → ℝ)
(hx : ∀ r ∈ Finset.Icc (jStar + 1) s, 0 ≤ x r)
:
∑ k ∈ Finset.Icc jStar s, profileRowWeight k s * ∑ r ∈ Finset.Icc (k + 1) s, x r ≤ 1 / (1 - 3 ^ (-(3 / 2))) * ∑ r ∈ Finset.Icc (jStar + 1) s, 3 ^ (-rhoDr * (↑s - ↑r)) * x r
The exchanged tail of the response row is bounded by the terminal
rhoDr-weighted increment row.
theorem
HCPolySupport.HighContrast.Response.profileRow_weighted_one_add_tail_le
{rhoDr : ℝ}
(hrho : rhoDr < 3 / 2)
{jStar s : ℤ}
(x : ℤ → ℝ)
(hx : ∀ r ∈ Finset.Icc (jStar + 1) s, 0 ≤ x r)
:
∑ k ∈ Finset.Icc jStar s, profileRowWeight k s * (1 + ∑ r ∈ Finset.Icc (k + 1) s, x r) ≤ (1 + ∑ r ∈ Finset.Icc (jStar + 1) s, 3 ^ (-rhoDr * (↑s - ↑r)) * x r) / (1 - 3 ^ (-(3 / 2)))
The complete finite row of terminal means has coefficient
(1 + D)/(1 - 3⁻³_right²).