High-contrast homogenization: Provider.PortableHistory.Geometric

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

The geometric weight of the nonlinear rows

The nonlinear rows of e.scale.selection.complete.profile carry the weights 3^{-a(T-1-j)} over j in a bounded range below T. Two of the estimates of p.fixed.geometry.one.grid.propagation — the additive part of the transported nonlinear row in e.fixed.geometry.profile.majorization, and the additive part of the contraction of the mean terms over one service step — bound the total weight by the geometric sum (1 - 3^{-a})^{-1}, uniformly in the endpoints.

The exponents are the nonnegative integers T - 1 - j, so the weight is the (T-1-j)-th power of the ratio 3^{-a} < 1, and the range is in bijection with an initial segment of the naturals.

The ratio

theorem HCPolySupport.HighContrast.PortableHistory.geom_ratio_lt_one {a : ℝ} (ha : 0 < a) : 3 ^ (-a) < 1

The geometric ratio of the nonlinear rows is strictly between zero and one.

theorem HCPolySupport.HighContrast.PortableHistory.geom_ratio_pos (a : ℝ) : 0 < 3 ^ (-a)

The geometric ratio of the nonlinear rows is positive.

The total weight

theorem HCPolySupport.HighContrast.PortableHistory.sum_geom_Ico_eq (a : ℝ) (b T : ℤ) : ∑ j ∈ Finset.Ico b T, 3 ^ (-a * (↑T - 1 - ↑j)) = ∑ k ∈ Finset.range (T - b).toNat, (3 ^ (-a)) ^ k

The weights of a nonlinear row form an initial segment of a geometric progression.

theorem HCPolySupport.HighContrast.PortableHistory.sum_geom_Ico_le {a : ℝ} (ha : 0 < a) (b T : ℤ) : ∑ j ∈ Finset.Ico b T, 3 ^ (-a * (↑T - 1 - ↑j)) ≤ 1 / (1 - 3 ^ (-a))

The total geometric weight of a nonlinear row. The weights 3^{-a(T-1-j)} over a bounded range below T sum to at most (1 - 3^{-a})^{-1}, uniformly in the endpoints.