feat(order/liminf_limsup): composition g ∘ f is bounded iff f is bounded (#14479)

* If `g` is a monotone function that tends to infinity at infinity, then a filter is bounded from above under `g ∘ f` iff it is bounded under `f`, similarly for antitone functions and/or filter bounded from below.
* A filter is bounded from above under `real.exp ∘ f` iff it is is bounded from above under `f`.
* Use `monotone` in `real.exp_monotone`.
* Add `@[mono]` to `real.exp_strict_mono`.

Author: urkud

src/analysis/special_functions/exp.lean

@@ -157,6 +157,14 @@ lemma tendsto_exp_at_bot : tendsto exp at_bot (𝓝 0) :=
 lemma tendsto_exp_at_bot_nhds_within : tendsto exp at_bot (𝓝[>] 0) :=
 tendsto_inf.2 ⟨tendsto_exp_at_bot, tendsto_principal.2 $ eventually_of_forall exp_pos⟩
 
+@[simp] lemma is_bounded_under_ge_exp_comp {α : Type*} (l : filter α) (f : α → ℝ) :
+  is_bounded_under (≥) l (λ x, exp (f x)) :=
+is_bounded_under_of ⟨0, λ x, (exp_pos _).le⟩
+
+@[simp] lemma is_bounded_under_le_exp_comp {α : Type*} {l : filter α} {f : α → ℝ} :
+  is_bounded_under (≤) l (λ x, exp (f x)) ↔ is_bounded_under (≤) l f :=
+exp_monotone.is_bounded_under_le_comp tendsto_exp_at_top
+
 /-- The function `exp(x)/x^n` tends to `+∞` at `+∞`, for any natural number `n` -/
 lemma tendsto_exp_div_pow_at_top (n : ℕ) : tendsto (λx, exp x / x^n) at_top at_top :=
 begin

src/data/complex/exponential.lean

@@ -1162,12 +1162,12 @@ lemma exp_pos (x : ℝ) : 0 < exp x :=
 @[simp] lemma abs_exp (x : ℝ) : |exp x| = exp x :=
 abs_of_pos (exp_pos _)
 
-lemma exp_strict_mono : strict_mono exp :=
+@[mono] lemma exp_strict_mono : strict_mono exp :=
 λ x y h, by rw [← sub_add_cancel y x, real.exp_add];
   exact (lt_mul_iff_one_lt_left (exp_pos _)).2
     (lt_of_lt_of_le (by linarith) (add_one_le_exp_of_nonneg (by linarith)))
 
-@[mono] lemma exp_monotone : ∀ {x y : ℝ}, x ≤ y → exp x ≤ exp y := exp_strict_mono.monotone
+@[mono] lemma exp_monotone : monotone exp := exp_strict_mono.monotone
 
 @[simp] lemma exp_lt_exp {x y : ℝ} : exp x < exp y ↔ x < y := exp_strict_mono.lt_iff_lt
 
@@ -1177,8 +1177,7 @@ lemma exp_injective : function.injective exp := exp_strict_mono.injective
 
 @[simp] lemma exp_eq_exp {x y : ℝ} : exp x = exp y ↔ x = y := exp_injective.eq_iff
 
-@[simp] lemma exp_eq_one_iff : exp x = 1 ↔ x = 0 :=
-by rw [← exp_zero, exp_injective.eq_iff]
+@[simp] lemma exp_eq_one_iff : exp x = 1 ↔ x = 0 := exp_injective.eq_iff' exp_zero
 
 @[simp] lemma one_lt_exp_iff {x : ℝ} : 1 < exp x ↔ 0 < x :=
 by rw [← exp_zero, exp_lt_exp]

src/order/liminf_limsup.lean

@@ -36,7 +36,7 @@ In complete lattices, however, it coincides with the `Inf Sup` definition.
 open filter set
 open_locale filter
 
-variables {α β ι : Type*}
+variables {α β γ ι : Type*}
 namespace filter
 
 section relation
@@ -510,7 +510,36 @@ end filter
 section order
 open filter
 
-lemma galois_connection.l_limsup_le {α β γ} [conditionally_complete_lattice β]
+lemma monotone.is_bounded_under_le_comp [nonempty β] [linear_order β] [preorder γ]
+  [no_max_order γ] {g : β → γ} {f : α → β} {l : filter α} (hg : monotone g)
+  (hg' : tendsto g at_top at_top) :
+  is_bounded_under (≤) l (g ∘ f) ↔ is_bounded_under (≤) l f :=
+begin
+  refine ⟨_, λ h, h.is_bounded_under hg⟩,
+  rintro ⟨c, hc⟩, rw eventually_map at hc,
+  obtain ⟨b, hb⟩ : ∃ b, ∀ a ≥ b, c < g a := eventually_at_top.1 (hg'.eventually_gt_at_top c),
+  exact ⟨b, hc.mono $ λ x hx, not_lt.1 (λ h, (hb _ h.le).not_le hx)⟩
+end
+
+lemma monotone.is_bounded_under_ge_comp [nonempty β] [linear_order β] [preorder γ]
+  [no_min_order γ] {g : β → γ} {f : α → β} {l : filter α} (hg : monotone g)
+  (hg' : tendsto g at_bot at_bot) :
+  is_bounded_under (≥) l (g ∘ f) ↔ is_bounded_under (≥) l f :=
+hg.dual.is_bounded_under_le_comp hg'
+
+lemma antitone.is_bounded_under_le_comp [nonempty β] [linear_order β] [preorder γ]
+  [no_max_order γ] {g : β → γ} {f : α → β} {l : filter α} (hg : antitone g)
+  (hg' : tendsto g at_bot at_top) :
+  is_bounded_under (≤) l (g ∘ f) ↔ is_bounded_under (≥) l f :=
+hg.dual_right.is_bounded_under_ge_comp hg'
+
+lemma antitone.is_bounded_under_ge_comp [nonempty β] [linear_order β] [preorder γ]
+  [no_min_order γ] {g : β → γ} {f : α → β} {l : filter α} (hg : antitone g)
+  (hg' : tendsto g at_top at_bot) :
+  is_bounded_under (≥) l (g ∘ f) ↔ is_bounded_under (≤) l f :=
+hg.dual_right.is_bounded_under_le_comp hg'
+
+lemma galois_connection.l_limsup_le [conditionally_complete_lattice β]
   [conditionally_complete_lattice γ] {f : filter α} {v : α → β}
   {l : β → γ} {u : γ → β} (gc : galois_connection l u)
   (hlv : f.is_bounded_under (≤) (λ x, l (v x)) . is_bounded_default)