Coarse-graining support: Support.Book.Ch05.Theorems.Section54.VarianceBoundGoodScale.GeometricSum

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

Elementary real estimates for the variance-bound sum

This file collects the low-level nonnegativity and square-root estimates used when summing the beta-weighted fluctuation bounds.

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.le_sqrt_of_nonneg_of_le_one {δ : ℝ} (hδ_nonneg : 0 ≤ δ) (hδ_le_one : δ ≤ 1) : δ ≤ √δ

The square root dominates δ on [0, 1].

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.le_sqrt_of_pos_of_le_half {δ : ℝ} (hδ_pos : 0 < δ) (hδ_le_half : δ ≤ 1 / 2) : δ ≤ √δ

In the manuscript range 0 < δ ≤ 1/2, the square root dominates δ.

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.sqrt_nonneg_of_pos {δ : ℝ} (_hδ_pos : 0 < δ) : 0 ≤ √δ

The square root of an admissible δ is nonnegative.

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.varianceWeight_mul_nonneg {β x : ℝ} {m j : ℕ} (hx : 0 ≤ x) : 0 ≤ varianceWeight β m j * x

A beta-weighted nonnegative term is nonnegative.

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.sum_Icc_varianceWeight_mul_nonneg {β : ℝ} {m : ℕ} {f : ℕ → ℝ} (hf : ∀ j ∈ Finset.Icc 1 m, 0 ≤ f j) : 0 ≤ ∑ j ∈ Finset.Icc 1 m, varianceWeight β m j * f j

A finite beta-weighted sum of nonnegative terms is nonnegative.

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.varianceWeight_mul_le_mul {β x y : ℝ} {m j : ℕ} (hxy : x ≤ y) : varianceWeight β m j * x ≤ varianceWeight β m j * y

Multiplication by a beta weight preserves an upper bound between nonnegative terms.

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.sum_Icc_varianceWeight_mul_le_mul {β : ℝ} {m : ℕ} {f g : ℕ → ℝ} (hfg : ∀ j ∈ Finset.Icc 1 m, f j ≤ g j) : ∑ j ∈ Finset.Icc 1 m, varianceWeight β m j * f j ≤ ∑ j ∈ Finset.Icc 1 m, varianceWeight β m j * g j

Sumwise version of varianceWeight_mul_le_mul.

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.sum_Icc_varianceWeight_mul_const (β c : ℝ) (m : ℕ) : ∑ j ∈ Finset.Icc 1 m, varianceWeight β m j * c = (∑ j ∈ Finset.Icc 1 m, varianceWeight β m j) * c

A constant can be pulled through a beta-weighted finite sum.

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.sum_Icc_varianceWeight_mul_le_const_mul {β C : ℝ} {m : ℕ} {f : ℕ → ℝ} (hf : ∀ j ∈ Finset.Icc 1 m, f j ≤ C) : ∑ j ∈ Finset.Icc 1 m, varianceWeight β m j * f j ≤ (∑ j ∈ Finset.Icc 1 m, varianceWeight β m j) * C

If C is nonnegative, enlarging a beta-weighted sum by a nonnegative constant preserves inequalities.

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.sum_Icc_varianceWeight_le_inv_geometricDiscount {β : ℝ} (hβ : 0 < β) (m : ℕ) : ∑ j ∈ Finset.Icc 1 m, varianceWeight β m j ≤ (geometricDiscount β 1)⁻¹

The finite beta-weight sum is bounded by the full geometric tail.