Mathlib.Analysis.SpecificLimits
Explicit bounds for polynomially weighted geometric series and related quantitative limit estimates.
PolynomialGeometric 1 core · 3 supporting This module supplies explicit geometric majorants for series whose terms are a polynomial weight times a geometric power. ★ polynomial_geometric_series_bound
Polynomially weighted geometric series
This module supplies explicit geometric majorants for series whose terms are a polynomial weight times a geometric power. The shift by two is convenient when the first relevant size is two, while the statements themselves are independent of any probabilistic application.
lemma polynomial_geometric_series_bound reviewed
⚑ flagged
Causalean.Mathlib.Analysis.SpecificLimits.PolynomialGeometric
For a natural exponent r and a real base z, when the base is nonnegative and 2^r times the base is at most one half, the series of (j+2)^r·z^(j+2) over all natural j is at most 2^(r+1)·z².
Formal statement
hypotheses
r :
ℕ
z :
ℝ
hz :
0 ≤ z
hsmall :
2 ^ r * z ≤ 1 / 2
conclusion
(∑' j : ℕ, (j + 2 : ℝ) ^ r * z ^ (j + 2)) ≤ 2 ^ (r + 1) * z ^ 2
Proof (Lean source)
lemma polynomial_geometric_series_bound (r : ℕ) (z : ℝ) (hz : 0 ≤ z)
(hsmall : 2 ^ r * z ≤ 1 / 2) :
(∑' j : ℕ, (j + 2 : ℝ) ^ r * z ^ (j + 2)) ≤ 2 ^ (r + 1) * z ^ 2 := by
have hratio : |(2 : ℝ) ^ r * z| < 1 := by
rw [abs_of_nonneg (by positivity)]
linarith
have hden : 0 < 1 - (2 : ℝ) ^ r * z := by linarith
calc
_ ≤ ∑' j : ℕ, 2 ^ r * z ^ 2 * (2 ^ r * z) ^ j :=
(polynomial_geometric_series_summable r z hz hsmall).tsum_le_tsum
(fun j => polynomial_geometric_term_le r j z hz)
((summable_geometric_of_abs_lt_one hratio).mul_left _)
_ = 2 ^ r * z ^ 2 / (1 - 2 ^ r * z) := by
rw [tsum_mul_left, tsum_geometric_of_abs_lt_one hratio, div_eq_mul_inv]
_ ≤ 2 ^ (r + 1) * z ^ 2 := by
apply (div_le_iff₀ hden).2
rw [pow_succ (2 : ℝ) r]
have hc : 0 ≤ (2 : ℝ) ^ r * z ^ 2 := by positivity
have hm := mul_le_mul_of_nonneg_left hsmall hc
nlinarith
3 supporting declarations (lemmas, instances)
-
nat_add_two_le_two_pow_succlemma — A natural-number index shifted by two is bounded by the corresponding dyadic power. The asserted bound holds.hypothesesj :ℕconclusion(j + 2 : ℝ) ≤ 2 ^ (j + 1)Proof (Lean source)
lemma nat_add_two_le_two_pow_succ (j : ℕ) : (j + 2 : ℝ) ≤ 2 ^ (j + 1) := by induction j with | zero => norm_num | succ j ih => rw [pow_succ] have hj : (0 : ℝ) ≤ j := Nat.cast_nonneg j push_cast nlinarith -
polynomial_geometric_term_lelemma — A polynomially weighted geometric term has an explicit geometric majorant when the base is nonnegative. The asserted termwise bound holds.hypothesesr j :ℕz :ℝhz :0 ≤ zconclusion(j + 2 : ℝ) ^ r * z ^ (j + 2) ≤ 2 ^ r * z ^ 2 * (2 ^ r * z) ^ jProof (Lean source)
lemma polynomial_geometric_term_le (r j : ℕ) (z : ℝ) (hz : 0 ≤ z) : (j + 2 : ℝ) ^ r * z ^ (j + 2) ≤ 2 ^ r * z ^ 2 * (2 ^ r * z) ^ j := by calc _ ≤ (2 ^ (j + 1) : ℝ) ^ r * z ^ (j + 2) := mul_le_mul_of_nonneg_right (pow_le_pow_left₀ (by positivity) (nat_add_two_le_two_pow_succ j) r) (pow_nonneg hz _) _ = _ := by rw [mul_pow, pow_add z j 2, ← pow_mul, ← pow_mul] rw [show (j + 1) * r = r + r * j by ring, pow_add] ring -
polynomial_geometric_series_summablelemma — A polynomially weighted geometric series is summable when the base is nonnegative and the explicit geometric ratio is at most one half. The asserted summability holds.hypothesesr :ℕz :ℝhz :0 ≤ zhsmall :2 ^ r * z ≤ 1 / 2conclusionSummable (fun j : ℕ => (j + 2 : ℝ) ^ r * z ^ (j + 2))Proof (Lean source)
lemma polynomial_geometric_series_summable (r : ℕ) (z : ℝ) (hz : 0 ≤ z) (hsmall : 2 ^ r * z ≤ 1 / 2) : Summable (fun j : ℕ => (j + 2 : ℝ) ^ r * z ^ (j + 2)) := by have hratio : |(2 : ℝ) ^ r * z| < 1 := by rw [abs_of_nonneg (by positivity)] linarith exact Summable.of_nonneg_of_le (fun _ => by positivity) (fun j => polynomial_geometric_term_le r j z hz) ((summable_geometric_of_abs_lt_one hratio).mul_left (2 ^ r * z ^ 2))