Coarse-graining support: Support.Deterministic.MultiscaleQuantitiesBasic.Foundation.GeometricOne

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

theorem HCPolySupport.geometricDiscount_nonneg {s q : ℝ} (hsq : 0 ≤ s * q) : 0 ≤ geometricDiscount s q

theorem HCPolySupport.geometricDiscount_pos {s q : ℝ} (hsq : 0 < s * q) : 0 < geometricDiscount s q

theorem HCPolySupport.geometricWeight_nonneg {s q : ℝ} (n : ℕ) (hsq : 0 ≤ s * q) : 0 ≤ geometricWeight s q n

theorem HCPolySupport.geometricWeight_pos {s q : ℝ} (n : ℕ) (hsq : 0 < s * q) : 0 < geometricWeight s q n

theorem HCPolySupport.summable_geometricWeight_one {s : ℝ} (hs : 0 < s) : Summable fun (n : ℕ) => geometricWeight s 1 n

theorem HCPolySupport.summable_geometricWeight_one_of_lt {H : ℕ → ℝ} (hnonneg : ∀ (n : ℕ), 0 ≤ H n) {t s : ℝ} (ht : 0 < t) (hts : t < s) (hsum_t : Summable fun (n : ℕ) => geometricWeight t 1 n * H n) : Summable fun (n : ℕ) => geometricWeight s 1 n * H n

theorem HCPolySupport.tsum_geometricWeight_one_eq_one {s : ℝ} (hs : 0 < s) : ∑' (n : ℕ), geometricWeight s 1 n = 1