feat(analysis/specific_limits): useful specializations of some lemmas (#12069)

Author: sgouezel

src/algebra/group_power/order.lean

@@ -191,6 +191,9 @@ strict_mono_pow h h2
 lemma pow_lt_pow_iff (h : 1 < a) : a ^ n < a ^ m ↔ n < m :=
 (strict_mono_pow h).lt_iff_lt
 
+lemma pow_le_pow_iff (h : 1 < a) : a ^ n ≤ a ^ m ↔ n ≤ m :=
+(strict_mono_pow h).le_iff_le
+
 lemma strict_anti_pow (h₀ : 0 < a) (h₁ : a < 1) : strict_anti (λ n : ℕ, a ^ n) :=
 strict_anti_nat_of_succ_lt $ λ n,
   by simpa only [pow_succ, one_mul] using mul_lt_mul h₁ le_rfl (pow_pos h₀ n) zero_le_one

src/analysis/normed/group/basic.lean

@@ -637,6 +637,10 @@ lemma add_sub_lipschitz_with (hf : antilipschitz_with Kf f) (hg : lipschitz_with
   (hK : Kg < Kf⁻¹) : antilipschitz_with (Kf⁻¹ - Kg)⁻¹ g :=
 by simpa only [pi.sub_apply, add_sub_cancel'_right] using hf.add_lipschitz_with hg hK
 
+lemma le_mul_norm_sub {f : E → F} (hf : antilipschitz_with K f) (x y : E) :
+  ∥x - y∥ ≤ K * ∥f x - f y∥ :=
+by simp [← dist_eq_norm, hf.le_mul_dist x y]
+
 end antilipschitz_with
 
 /-- A group homomorphism from an `add_comm_group` to a `semi_normed_group` induces a

src/analysis/specific_limits.lean

@@ -304,6 +304,24 @@ begin
   simpa [div_eq_mul_inv] using tendsto_pow_const_div_const_pow_of_one_lt k hr'
 end
 
+/-- If `0 ≤ r < 1`, then `n ^ k r ^ n` tends to zero for any natural `k`.
+This is a specialized version of `tendsto_pow_const_mul_const_pow_of_abs_lt_one`, singled out
+for ease of application. -/
+lemma tendsto_pow_const_mul_const_pow_of_lt_one (k : ℕ) {r : ℝ} (hr : 0 ≤ r) (h'r : r < 1) :
+  tendsto (λ n, n ^ k * r ^ n : ℕ → ℝ) at_top (𝓝 0) :=
+tendsto_pow_const_mul_const_pow_of_abs_lt_one k (abs_lt.2 ⟨neg_one_lt_zero.trans_le hr, h'r⟩)
+
+/-- If `|r| < 1`, then `n * r ^ n` tends to zero. -/
+lemma tendsto_self_mul_const_pow_of_abs_lt_one {r : ℝ} (hr : |r| < 1) :
+  tendsto (λ n, n * r ^ n : ℕ → ℝ) at_top (𝓝 0) :=
+by simpa only [pow_one] using tendsto_pow_const_mul_const_pow_of_abs_lt_one 1 hr
+
+/-- If `0 ≤ r < 1`, then `n * r ^ n` tends to zero. This is a specialized version of
+`tendsto_self_mul_const_pow_of_abs_lt_one`, singled out for ease of application. -/
+lemma tendsto_self_mul_const_pow_of_lt_one {r : ℝ} (hr : 0 ≤ r) (h'r : r < 1) :
+  tendsto (λ n, n * r ^ n : ℕ → ℝ) at_top (𝓝 0) :=
+by simpa only [pow_one] using tendsto_pow_const_mul_const_pow_of_lt_one 1 hr h'r
+
 /-- If a sequence `v` of real numbers satisfies `k * v n ≤ v (n+1)` with `1 < k`,
 then it goes to +∞. -/
 lemma tendsto_at_top_of_geom_le {v : ℕ → ℝ} {c : ℝ} (h₀ : 0 < v 0) (hc : 1 < c)
@@ -361,6 +379,10 @@ by convert has_sum_geometric_of_lt_1 _ _; norm_num
 lemma summable_geometric_two : summable (λn:ℕ, ((1:ℝ)/2) ^ n) :=
 ⟨_, has_sum_geometric_two⟩
 
+lemma summable_geometric_two_encode {ι : Type*} [encodable ι] :
+  summable (λ (i : ι), (1/2 : ℝ)^(encodable.encode i)) :=
+summable_geometric_two.comp_injective encodable.encode_injective
+
 lemma tsum_geometric_two : ∑'n:ℕ, ((1:ℝ)/2) ^ n = 2 :=
 has_sum_geometric_two.tsum_eq