From a3beb6282deccf44f3f07746ce8390ff6305d410 Mon Sep 17 00:00:00 2001
From: sgouezel <sebastien.gouezel@univ-rennes1.fr>
Date: Fri, 29 Apr 2022 14:39:18 +0000
Subject: [PATCH] feat(analysis/*): a sample of easy useful lemmas (#13697)

Lemmas needed for #13690
---
 src/analysis/inner_product_space/pi_L2.lean | 17 +++++------------
 src/analysis/special_functions/pow.lean     | 16 ++++++++++++++--
 src/analysis/specific_limits/basic.lean     | 12 ++++++++++++
 src/data/real/ennreal.lean                  |  1 +
 src/topology/algebra/group.lean             |  9 +++++++++
 5 files changed, 41 insertions(+), 14 deletions(-)

diff --git a/src/analysis/inner_product_space/pi_L2.lean b/src/analysis/inner_product_space/pi_L2.lean
index e02c49dda1d93..774acfea5dc85 100644
--- a/src/analysis/inner_product_space/pi_L2.lean
+++ b/src/analysis/inner_product_space/pi_L2.lean
@@ -57,17 +57,11 @@ instance pi_Lp.inner_product_space {ι : Type*} [fintype ι] (f : ι → Type*)
   norm_sq_eq_inner :=
   begin
     intro x,
-    have h₁ : ∑ (i : ι), ∥x i∥ ^ (2 : ℕ) = ∑ (i : ι), ∥x i∥ ^ (2 : ℝ),
-    { apply finset.sum_congr rfl,
-      intros j hj,
-      simp [←rpow_nat_cast] },
-    have h₂ : 0 ≤ ∑ (i : ι), ∥x i∥ ^ (2 : ℝ),
-    { rw [←h₁],
-      exact finset.sum_nonneg (λ j (hj : j ∈ finset.univ), pow_nonneg (norm_nonneg (x j)) 2) },
-    simp [norm, add_monoid_hom.map_sum, ←norm_sq_eq_inner],
-    rw [←rpow_nat_cast ((∑ (i : ι), ∥x i∥ ^ (2 : ℝ)) ^ (2 : ℝ)⁻¹) 2],
-    rw [←rpow_mul h₂],
-    norm_num [h₁],
+    have h₂ : 0 ≤ ∑ (i : ι), ∥x i∥ ^ (2 : ℝ) :=
+      finset.sum_nonneg (λ j hj, rpow_nonneg_of_nonneg (norm_nonneg (x j)) 2),
+    simp only [norm, add_monoid_hom.map_sum, ← norm_sq_eq_inner, one_div],
+    rw [← rpow_nat_cast ((∑ (i : ι), ∥x i∥ ^ (2 : ℝ)) ^ (2 : ℝ)⁻¹) 2, ← rpow_mul h₂],
+    norm_num,
   end,
   conj_sym :=
   begin
@@ -483,4 +477,3 @@ lemma inner_matrix_col_col (A B : matrix (fin n) (fin m) 𝕜) (i j : (fin m)) :
   ⟪Aᵀ i, Bᵀ j⟫ₙ = (Aᴴ ⬝ B) i j := rfl
 
 end matrix
-
diff --git a/src/analysis/special_functions/pow.lean b/src/analysis/special_functions/pow.lean
index 916c3db4e14f6..f24b1db182652 100644
--- a/src/analysis/special_functions/pow.lean
+++ b/src/analysis/special_functions/pow.lean
@@ -99,13 +99,16 @@ by rw [sub_eq_add_neg, cpow_add _ _ hx, cpow_neg, div_eq_mul_inv]
 lemma cpow_neg_one (x : ℂ) : x ^ (-1 : ℂ) = x⁻¹ :=
 by simpa using cpow_neg x 1
 
-@[simp] lemma cpow_nat_cast (x : ℂ) : ∀ (n : ℕ), x ^ (n : ℂ) = x ^ n
+@[simp, norm_cast] lemma cpow_nat_cast (x : ℂ) : ∀ (n : ℕ), x ^ (n : ℂ) = x ^ n
 | 0       := by simp
 | (n + 1) := if hx : x = 0 then by simp only [hx, pow_succ,
     complex.zero_cpow (nat.cast_ne_zero.2 (nat.succ_ne_zero _)), zero_mul]
   else by simp [cpow_add, hx, pow_add, cpow_nat_cast n]
 
-@[simp] lemma cpow_int_cast (x : ℂ) : ∀ (n : ℤ), x ^ (n : ℂ) = x ^ n
+@[simp] lemma cpow_two (x : ℂ) : x ^ (2 : ℂ) = x ^ 2 :=
+by { rw ← cpow_nat_cast, simp only [nat.cast_bit0, nat.cast_one] }
+
+@[simp, norm_cast] lemma cpow_int_cast (x : ℂ) : ∀ (n : ℤ), x ^ (n : ℂ) = x ^ n
 | (n : ℕ) := by simp; refl
 | -[1+ n] := by rw zpow_neg_succ_of_nat;
   simp only [int.neg_succ_of_nat_coe, int.cast_neg, complex.cpow_neg, inv_eq_one_div,
@@ -529,6 +532,9 @@ by simp only [rpow_def, ← complex.of_real_zpow, complex.cpow_int_cast,
 @[simp, norm_cast] lemma rpow_nat_cast (x : ℝ) (n : ℕ) : x ^ (n : ℝ) = x ^ n :=
 rpow_int_cast x n
 
+@[simp] lemma rpow_two (x : ℝ) : x ^ (2 : ℝ) = x ^ 2 :=
+by { rw ← rpow_nat_cast, simp only [nat.cast_bit0, nat.cast_one] }
+
 lemma rpow_neg_one (x : ℝ) : x ^ (-1 : ℝ) = x⁻¹ :=
 begin
   suffices H : x ^ ((-1 : ℤ) : ℝ) = x⁻¹, by exact_mod_cast H,
@@ -1109,6 +1115,9 @@ end
 @[simp, norm_cast] lemma rpow_nat_cast (x : ℝ≥0) (n : ℕ) : x ^ (n : ℝ) = x ^ n :=
 nnreal.eq $ by simpa only [coe_rpow, coe_pow] using real.rpow_nat_cast x n
 
+@[simp] lemma rpow_two (x : ℝ≥0) : x ^ (2 : ℝ) = x ^ 2 :=
+by { rw ← rpow_nat_cast, simp only [nat.cast_bit0, nat.cast_one] }
+
 lemma mul_rpow {x y : ℝ≥0} {z : ℝ}  : (x*y)^z = x^z * y^z :=
 nnreal.eq $ real.mul_rpow x.2 y.2
 
@@ -1445,6 +1454,9 @@ begin
   { simp [coe_rpow_of_nonneg _ (nat.cast_nonneg n)] }
 end
 
+@[simp] lemma rpow_two (x : ℝ≥0∞) : x ^ (2 : ℝ) = x ^ 2 :=
+by { rw ← rpow_nat_cast, simp only [nat.cast_bit0, nat.cast_one] }
+
 lemma mul_rpow_eq_ite (x y : ℝ≥0∞) (z : ℝ) :
   (x * y) ^ z = if (x = 0 ∧ y = ⊤ ∨ x = ⊤ ∧ y = 0) ∧ z < 0 then ⊤ else x ^ z * y ^ z :=
 begin
diff --git a/src/analysis/specific_limits/basic.lean b/src/analysis/specific_limits/basic.lean
index 9da442f36a75d..1753382c4a033 100644
--- a/src/analysis/specific_limits/basic.lean
+++ b/src/analysis/specific_limits/basic.lean
@@ -514,6 +514,10 @@ tendsto_of_tendsto_of_tendsto_of_le_of_le'
 
 section
 
+lemma tendsto_nat_floor_at_top {α : Type*} [linear_ordered_semiring α] [floor_semiring α] :
+  tendsto (λ (x : α), ⌊x⌋₊) at_top at_top :=
+nat.floor_mono.tendsto_at_top_at_top (λ x, ⟨max 0 (x + 1), by simp [nat.le_floor_iff]⟩)
+
 variables {R : Type*} [topological_space R] [linear_ordered_field R] [order_topology R]
 [floor_ring R]
 
@@ -534,6 +538,10 @@ begin
     simp [nat.floor_le (mul_nonneg ha (zero_le_one.trans hx))] }
 end
 
+lemma tendsto_nat_floor_div_at_top :
+  tendsto (λ x, (⌊x⌋₊ : R) / x) at_top (𝓝 1) :=
+by simpa using tendsto_nat_floor_mul_div_at_top (@zero_le_one R _)
+
 lemma tendsto_nat_ceil_mul_div_at_top {a : R} (ha : 0 ≤ a) :
   tendsto (λ x, (⌈a * x⌉₊ : R) / x) at_top (𝓝 a) :=
 begin
@@ -549,4 +557,8 @@ begin
       (nat.ceil_lt_add_one ((mul_nonneg ha (zero_le_one.trans hx)))).le, add_mul] }
 end
 
+lemma tendsto_nat_ceil_div_at_top :
+  tendsto (λ x, (⌈x⌉₊ : R) / x) at_top (𝓝 1) :=
+by simpa using tendsto_nat_ceil_mul_div_at_top (@zero_le_one R _)
+
 end
diff --git a/src/data/real/ennreal.lean b/src/data/real/ennreal.lean
index 344c3bb088bc4..446b17bb3b5c3 100644
--- a/src/data/real/ennreal.lean
+++ b/src/data/real/ennreal.lean
@@ -224,6 +224,7 @@ protected lemma zero_lt_one : 0 < (1 : ℝ≥0∞) :=
 
 @[simp] lemma one_lt_two : (1 : ℝ≥0∞) < 2 :=
 coe_one ▸ coe_two ▸ by exact_mod_cast (@one_lt_two ℕ _ _)
+lemma one_le_two : (1 : ℝ≥0∞) ≤ 2 := one_lt_two.le
 @[simp] lemma zero_lt_two : (0:ℝ≥0∞) < 2 := lt_trans ennreal.zero_lt_one one_lt_two
 lemma two_ne_zero : (2:ℝ≥0∞) ≠ 0 := (ne_of_lt zero_lt_two).symm
 lemma two_ne_top : (2:ℝ≥0∞) ≠ ∞ := coe_two ▸ coe_ne_top
diff --git a/src/topology/algebra/group.lean b/src/topology/algebra/group.lean
index 6321a138971f0..c966322f5f58c 100644
--- a/src/topology/algebra/group.lean
+++ b/src/topology/algebra/group.lean
@@ -894,6 +894,15 @@ lemma is_open_map_div_right (a : G) : is_open_map (λ x, x / a) :=
 lemma is_closed_map_div_right (a : G) : is_closed_map (λ x, x / a) :=
 (homeomorph.div_right a).is_closed_map
 
+@[to_additive]
+lemma tendsto_div_nhds_one_iff
+  {α : Type*} {l : filter α} {x : G} {u : α → G} :
+  tendsto (λ n, u n / x) l (𝓝 1) ↔ tendsto u l (𝓝 x) :=
+begin
+  have A : tendsto (λ (n : α), x) l (𝓝 x) := tendsto_const_nhds,
+  exact ⟨λ h, by simpa using h.mul A, λ h, by simpa using h.div' A⟩
+end
+
 end div_in_topological_group
 
 @[to_additive]