feat(analysis/special_functions): lemmas about filter map/comap (#…

…14513)

* add `comap_inf_principal_range` and `comap_nhds_within_range`;
* add `@[simp]` to `real.comap_exp_nhds_within_Ioi_zero`;
* add `real.comap_exp_nhds_zero`, `complex.comap_exp_comap_abs_at_top`, `complex.comap_exp_nhds_zero`, `complex.comap_exp_nhds_within_zero`, and `complex.tendsto_exp_nhds_zero_iff`;
* add `complex.map_exp_comap_re_at_bot` and `complex.map_exp_comap_re_at_top`;
* add `comap_norm_nhds_zero` and `complex.comap_abs_nhds_zero`.

src/analysis/complex/basic.lean

@@ -33,7 +33,7 @@ noncomputable theory
 
 namespace complex
 
-open_locale complex_conjugate
+open_locale complex_conjugate topological_space
 
 instance : has_norm ℂ := ⟨abs⟩
 
@@ -77,6 +77,8 @@ by simp only [dist_eq, sub_conj, of_real_mul, of_real_bit0, of_real_one, abs_mul
 lemma dist_conj_self (z : ℂ) : dist (conj z) z = 2 * |z.im| :=
 by rw [dist_comm, dist_self_conj]
 
+@[simp] lemma comap_abs_nhds_zero : filter.comap abs (𝓝 0) = 𝓝 0 := comap_norm_nhds_zero
+
 @[simp] lemma norm_real (r : ℝ) : ∥(r : ℂ)∥ = ∥r∥ := abs_of_real _
 
 @[simp] lemma norm_rat (r : ℚ) : ∥(r : ℂ)∥ = |(r : ℝ)| :=

src/analysis/normed/group/basic.lean

@@ -875,6 +875,9 @@ lemma tendsto_zero_iff_norm_tendsto_zero {f : α → E} {a : filter α} :
   tendsto f a (𝓝 0) ↔ tendsto (λ e, ∥f e∥) a (𝓝 0) :=
 by { rw [tendsto_iff_norm_tendsto_zero], simp only [sub_zero] }
 
+lemma comap_norm_nhds_zero : comap norm (𝓝 0) = 𝓝 (0 : E) :=
+by simpa only [dist_zero_right] using nhds_comap_dist (0 : E)
+
 /-- Special case of the sandwich theorem: if the norm of `f` is eventually bounded by a real
 function `g` which tends to `0`, then `f` tends to `0`.
 In this pair of lemmas (`squeeze_zero_norm'` and `squeeze_zero_norm`), following a convention of

src/analysis/special_functions/complex/log.lean

@@ -133,6 +133,15 @@ lemma tendsto_log_nhds_within_im_nonneg_of_re_neg_of_im_zero
 by simpa only [log, arg_eq_pi_iff.2 ⟨hre, him⟩]
   using (continuous_within_at_log_of_re_neg_of_im_zero hre him).tendsto
 
+@[simp] lemma map_exp_comap_re_at_bot : map exp (comap re at_bot) = 𝓝[≠] 0 :=
+by rw [← comap_exp_nhds_zero, map_comap, range_exp, nhds_within]
+
+@[simp] lemma map_exp_comap_re_at_top : map exp (comap re at_top) = comap abs at_top :=
+begin
+  rw [← comap_exp_comap_abs_at_top, map_comap, range_exp, inf_eq_left, le_principal_iff],
+  exact eventually_ne_of_tendsto_norm_at_top tendsto_comap 0
+end
+
 end complex
 
 section log_deriv

src/analysis/special_functions/exp.lean

@@ -256,13 +256,16 @@ by rw [← tendsto_map'_iff, map_exp_at_top]
 @[simp] lemma map_exp_at_bot : map exp at_bot = 𝓝[>] 0 :=
 by rw [← coe_comp_exp_order_iso, ← filter.map_map, exp_order_iso.map_at_bot, ← map_coe_Ioi_at_bot]
 
-lemma comap_exp_nhds_within_Ioi_zero : comap exp (𝓝[>] 0) = at_bot :=
+@[simp] lemma comap_exp_nhds_within_Ioi_zero : comap exp (𝓝[>] 0) = at_bot :=
 by rw [← map_exp_at_bot, comap_map exp_injective]
 
 lemma tendsto_comp_exp_at_bot {α : Type*} {l : filter α} {f : ℝ → α} :
   tendsto (λ x, f (exp x)) at_bot l ↔ tendsto f (𝓝[>] 0) l :=
 by rw [← map_exp_at_bot, tendsto_map'_iff]
 
+@[simp] lemma comap_exp_nhds_zero : comap exp (𝓝 0) = at_bot :=
+(comap_nhds_within_range exp 0).symm.trans $ by simp
+
 lemma is_o_pow_exp_at_top {n : ℕ} : (λ x, x^n) =o[at_top] real.exp :=
 by simpa [is_o_iff_tendsto (λ x hx, ((exp_pos x).ne' hx).elim)]
   using tendsto_div_pow_mul_exp_add_at_top 1 0 n zero_ne_one
@@ -271,17 +274,33 @@ end real
 
 namespace complex
 
+lemma comap_exp_comap_abs_at_top : comap exp (comap abs at_top) = comap re at_top :=
+calc comap exp (comap abs at_top) = comap re (comap real.exp at_top) :
+  by simp only [comap_comap, (∘), abs_exp]
+... = comap re at_top : by rw [real.comap_exp_at_top]
+
+lemma comap_exp_nhds_zero : comap exp (𝓝 0) = comap re at_bot :=
+calc comap exp (𝓝 0) = comap re (comap real.exp (𝓝 0)) :
+  by simp only [comap_comap, ← comap_abs_nhds_zero, (∘), abs_exp]
+... = comap re at_bot : by rw [real.comap_exp_nhds_zero]
+
+lemma comap_exp_nhds_within_zero : comap exp (𝓝[≠] 0) = comap re at_bot :=
+have exp ⁻¹' {0}ᶜ = univ, from eq_univ_of_forall exp_ne_zero,
+by simp [nhds_within, comap_exp_nhds_zero, this]
+
+lemma tendsto_exp_nhds_zero_iff {α : Type*} {l : filter α} {f : α → ℂ} :
+  tendsto (λ x, exp (f x)) l (𝓝 0) ↔ tendsto (λ x, re (f x)) l at_bot :=
+by rw [← tendsto_comap_iff, comap_exp_nhds_zero, tendsto_comap_iff]
+
 /-- `complex.abs (complex.exp z) → ∞` as `complex.re z → ∞`. TODO: use `bornology.cobounded`. -/
 lemma tendsto_exp_comap_re_at_top : tendsto exp (comap re at_top) (comap abs at_top) :=
-by simpa only [tendsto_comap_iff, (∘), abs_exp] using real.tendsto_exp_at_top.comp tendsto_comap
+comap_exp_comap_abs_at_top ▸ tendsto_comap
 
 /-- `complex.exp z → 0` as `complex.re z → -∞`.-/
 lemma tendsto_exp_comap_re_at_bot : tendsto exp (comap re at_bot) (𝓝 0) :=
-tendsto_zero_iff_norm_tendsto_zero.2 $
-  by simpa only [norm_eq_abs, abs_exp] using real.tendsto_exp_at_bot.comp tendsto_comap
+comap_exp_nhds_zero ▸ tendsto_comap
 
 lemma tendsto_exp_comap_re_at_bot_nhds_within : tendsto exp (comap re at_bot) (𝓝[≠] 0) :=
-tendsto_inf.2 ⟨tendsto_exp_comap_re_at_bot,
-  tendsto_principal.2 $ eventually_of_forall $ exp_ne_zero⟩
+comap_exp_nhds_within_zero ▸ tendsto_comap
 
 end complex

src/order/filter/basic.lean

@@ -1706,7 +1706,9 @@ lemma map_comap_le : map m (comap m g) ≤ g := (gc_map_comap m).l_u_le _
 lemma le_comap_map : f ≤ comap m (map m f) := (gc_map_comap m).le_u_l _
 
 @[simp] lemma comap_bot : comap m ⊥ = ⊥ :=
-bot_unique $ λ s _, ⟨∅, by simp only [mem_bot], by simp only [empty_subset, preimage_empty]⟩
+bot_unique $ λ s _, ⟨∅, mem_bot, by simp only [empty_subset, preimage_empty]⟩
+
+lemma comap_inf_principal_range : comap m (g ⊓ 𝓟 (range m)) = comap m g := by simp
 
 lemma disjoint_comap (h : disjoint g₁ g₂) : disjoint (comap m g₁) (comap m g₂) :=
 by simp only [disjoint_iff, ← comap_inf, h.eq_bot, comap_bot]

src/topology/continuous_on.lean

@@ -552,7 +552,11 @@ hs.induction_on (continuous_on_empty f) (continuous_on_singleton f)
 
 theorem nhds_within_le_comap {x : α} {s : set α} {f : α → β} (ctsf : continuous_within_at f s x) :
   𝓝[s] x ≤ comap f (𝓝[f '' s] (f x)) :=
-map_le_iff_le_comap.1 ctsf.tendsto_nhds_within_image
+ctsf.tendsto_nhds_within_image.le_comap
+
+@[simp] lemma comap_nhds_within_range {α} (f : α → β) (y : β) :
+  comap f (𝓝[range f] y) = comap f (𝓝 y) :=
+comap_inf_principal_range
 
 theorem continuous_within_at_iff_ptendsto_res (f : α → β) {x : α} {s : set α} :
   continuous_within_at f s x ↔ ptendsto (pfun.res f s) (𝓝 x) (𝓝 (f x)) :=