chore(topology/algebra/*,analysis/specific_limits): continuity of fpow (#8665)

* add more API lemmas about continuity of `x ^ n` for natural and integer `n`;
* prove that `x⁻¹` and `x ^ n`, `n < 0`, are discontinuous at zero.

Author: urkud

src/algebra/group/basic.lean

@@ -190,6 +190,10 @@ inv_inv
 @[simp, to_additive]
 lemma inv_involutive : function.involutive (has_inv.inv : G → G) := inv_inv
 
+@[simp, to_additive]
+lemma inv_surjective : function.surjective (has_inv.inv : G → G) :=
+inv_involutive.surjective
+
 @[to_additive]
 lemma inv_injective : function.injective (has_inv.inv : G → G) :=
 inv_involutive.injective

src/analysis/fourier.lean

@@ -87,7 +87,7 @@ section fourier
 continuous maps from `circle` to `ℂ`. -/
 @[simps] def fourier (n : ℤ) : C(circle, ℂ) :=
 { to_fun := λ z, z ^ n,
-  continuous_to_fun := continuous_subtype_coe.fpow nonzero_of_mem_circle n }
+  continuous_to_fun := continuous_subtype_coe.fpow n $ λ z, or.inl (nonzero_of_mem_circle z) }
 
 @[simp] lemma fourier_zero {z : circle} : fourier 0 z = 1 := rfl
 

src/analysis/specific_limits.lean

@@ -69,13 +69,40 @@ nat.sub_add_cancel (le_of_lt h) ▸
   tendsto_add_one_pow_at_top_at_top_of_pos (nat.sub_pos_of_lt h)
 
 lemma tendsto_norm_zero' {𝕜 : Type*} [normed_group 𝕜] :
-  tendsto (norm : 𝕜 → ℝ) (𝓝[{x | x ≠ 0}] 0) (𝓝[set.Ioi 0] 0) :=
+  tendsto (norm : 𝕜 → ℝ) (𝓝[{0}ᶜ] 0) (𝓝[set.Ioi 0] 0) :=
 tendsto_norm_zero.inf $ tendsto_principal_principal.2 $ λ x hx, norm_pos_iff.2 hx
 
-lemma normed_field.tendsto_norm_inverse_nhds_within_0_at_top {𝕜 : Type*} [normed_field 𝕜] :
-  tendsto (λ x:𝕜, ∥x⁻¹∥) (𝓝[{x | x ≠ 0}] 0) at_top :=
+namespace normed_field
+
+lemma tendsto_norm_inverse_nhds_within_0_at_top {𝕜 : Type*} [normed_field 𝕜] :
+  tendsto (λ x:𝕜, ∥x⁻¹∥) (𝓝[{0}ᶜ] 0) at_top :=
 (tendsto_inv_zero_at_top.comp tendsto_norm_zero').congr $ λ x, (normed_field.norm_inv x).symm
 
+lemma tendsto_norm_fpow_nhds_within_0_at_top {𝕜 : Type*} [normed_field 𝕜] {m : ℤ}
+  (hm : m < 0) :
+  tendsto (λ x : 𝕜, ∥x ^ m∥) (𝓝[{0}ᶜ] 0) at_top :=
+begin
+  rcases neg_surjective m with ⟨m, rfl⟩,
+  rw neg_lt_zero at hm, lift m to ℕ using hm.le, rw int.coe_nat_pos at hm,
+  simp only [normed_field.norm_pow, fpow_neg, gpow_coe_nat, ← inv_pow'],
+  exact (tendsto_pow_at_top hm).comp normed_field.tendsto_norm_inverse_nhds_within_0_at_top
+end
+
+@[simp] lemma continuous_at_fpow {𝕜 : Type*} [nondiscrete_normed_field 𝕜] {m : ℤ} {x : 𝕜} :
+  continuous_at (λ x, x ^ m) x ↔ x ≠ 0 ∨ 0 ≤ m :=
+begin
+  refine ⟨_, continuous_at_fpow _ _⟩,
+  contrapose!, rintro ⟨rfl, hm⟩ hc,
+  exact not_tendsto_at_top_of_tendsto_nhds (hc.tendsto.mono_left nhds_within_le_nhds).norm
+      (tendsto_norm_fpow_nhds_within_0_at_top hm)
+end
+
+@[simp] lemma continuous_at_inv {𝕜 : Type*} [nondiscrete_normed_field 𝕜] {x : 𝕜} :
+  continuous_at has_inv.inv x ↔ x ≠ 0 :=
+by simpa [(@zero_lt_one ℤ _ _).not_le] using @continuous_at_fpow _ _ (-1) x
+
+end normed_field
+
 lemma tendsto_pow_at_top_nhds_0_of_lt_1 {𝕜 : Type*} [linear_ordered_field 𝕜] [archimedean 𝕜]
   [topological_space 𝕜] [order_topology 𝕜] {r : 𝕜} (h₁ : 0 ≤ r) (h₂ : r < 1) :
   tendsto (λn:ℕ, r^n) at_top (𝓝 0) :=

src/topology/algebra/group_with_zero.lean

@@ -206,44 +206,39 @@ section fpow
 variables [group_with_zero G₀] [topological_space G₀] [has_continuous_inv' G₀]
   [has_continuous_mul G₀]
 
-lemma tendsto_fpow {x : G₀} (hx : x ≠ 0) (m : ℤ) : tendsto (λ x, x ^ m) (𝓝 x) (𝓝 (x ^ m)) :=
+lemma continuous_at_fpow (x : G₀) (m : ℤ) (h : x ≠ 0 ∨ 0 ≤ m) : continuous_at (λ x, x ^ m) x :=
 begin
-  have : ∀ y : G₀, ∀ m : ℤ, 0 < m → tendsto (λ x, x ^ m) (𝓝 y) (𝓝 (y ^ m)),
-  { assume y m hm,
-    lift m to ℕ using (le_of_lt hm) with k,
-    simp only [gpow_coe_nat],
-    exact (continuous_pow k).continuous_at.tendsto },
-  rcases lt_trichotomy m 0 with hm | hm | hm,
-  { have hm' : 0 < - m := by rwa neg_pos,
-    convert (this _ (-m) hm').comp (tendsto_inv' hx) using 1,
-    { ext y,
-      simp },
-    { congr' 1,
-      simp } },
-  { simpa [hm] using tendsto_const_nhds },
-  { exact this _ m hm }
+  cases m,
+  { simpa only [gpow_of_nat] using continuous_at_pow x m },
+  { simp only [gpow_neg_succ_of_nat],
+    have hx : x ≠ 0, from h.resolve_right (int.neg_succ_of_nat_lt_zero m).not_le,
+    exact (continuous_at_pow x (m + 1)).inv' (pow_ne_zero _ hx) }
 end
 
-lemma continuous_at_fpow {x : G₀} (hx : x ≠ 0) (m : ℤ) : continuous_at (λ x, x ^ m) x :=
-tendsto_fpow hx m
-
 lemma continuous_on_fpow (m : ℤ) : continuous_on (λ x : G₀, x ^ m) {0}ᶜ :=
-λ x hx, (continuous_at_fpow hx m).continuous_within_at
-
-variables {f : α → G₀}
+λ x hx, (continuous_at_fpow _ _ (or.inl hx)).continuous_within_at
 
-lemma filter.tendsto.fpow {l : filter α} {a : G₀} (hf : tendsto f l (𝓝 a)) (ha : a ≠ 0) (m : ℤ) :
+lemma filter.tendsto.fpow {f : α → G₀} {l : filter α} {a : G₀} (hf : tendsto f l (𝓝 a)) (m : ℤ)
+  (h : a ≠ 0 ∨ 0 ≤ m) :
   tendsto (λ x, (f x) ^ m) l (𝓝 (a ^ m)) :=
-(tendsto_fpow ha m).comp hf
+(continuous_at_fpow _ m h).tendsto.comp hf
 
-variables [topological_space α] {a : α}
+variables {X : Type*} [topological_space X] {a : X} {s : set X} {f : X → G₀}
 
-lemma continuous_at.fpow (hf : continuous_at f a) (ha : f a ≠ 0) (m : ℤ) :
+lemma continuous_at.fpow (hf : continuous_at f a) (m : ℤ) (h : f a ≠ 0 ∨ 0 ≤ m) :
   continuous_at (λ x, (f x) ^ m) a :=
-(continuous_at_fpow ha m).comp hf
+hf.fpow m h
+
+lemma continuous_within_at.fpow (hf : continuous_within_at f s a) (m : ℤ) (h : f a ≠ 0 ∨ 0 ≤ m) :
+  continuous_within_at (λ x, f x ^ m) s a :=
+hf.fpow m h
+
+lemma continuous_on.fpow (hf : continuous_on f s) (m : ℤ) (h : ∀ a ∈ s, f a ≠ 0 ∨ 0 ≤ m) :
+  continuous_on (λ x, f x ^ m) s :=
+λ a ha, (hf a ha).fpow m (h a ha)
 
-@[continuity] lemma continuous.fpow (hf : continuous f) (h0 : ∀ a, f a ≠ 0) (m : ℤ) :
+@[continuity] lemma continuous.fpow (hf : continuous f) (m : ℤ) (h0 : ∀ a, f a ≠ 0 ∨ 0 ≤ m) :
   continuous (λ x, (f x) ^ m) :=
-continuous_iff_continuous_at.2 $ λ x, (hf.tendsto x).fpow (h0 x) m
+continuous_iff_continuous_at.2 $ λ x, (hf.tendsto x).fpow m (h0 x)
 
 end fpow

src/topology/algebra/monoid.lean

@@ -278,6 +278,25 @@ lemma continuous.pow {f : X → M} (h : continuous f) (n : ℕ) :
 lemma continuous_on_pow {s : set M} (n : ℕ) : continuous_on (λ x, x ^ n) s :=
 (continuous_pow n).continuous_on
 
+lemma continuous_at_pow (x : M) (n : ℕ) : continuous_at (λ x, x ^ n) x :=
+(continuous_pow n).continuous_at
+
+lemma filter.tendsto.pow {l : filter α} {f : α → M} {x : M} (hf : tendsto f l (𝓝 x)) (n : ℕ) :
+  tendsto (λ x, f x ^ n) l (𝓝 (x ^ n)) :=
+(continuous_at_pow _ _).tendsto.comp hf
+
+lemma continuous_within_at.pow {f : X → M} {x : X} {s : set X} (hf : continuous_within_at f s x)
+  (n : ℕ) : continuous_within_at (λ x, f x ^ n) s x :=
+hf.pow n
+
+lemma continuous_at.pow {f : X → M} {x : X} (hf : continuous_at f x) (n : ℕ) :
+  continuous_at (λ x, f x ^ n) x :=
+hf.pow n
+
+lemma continuous_on.pow {f : X → M} {s : set X} (hf : continuous_on f s) (n : ℕ) :
+  continuous_on (λ x, f x ^ n) s :=
+λ x hx, (hf x hx).pow n
+
 end has_continuous_mul
 
 section op