refactor(analysis/asymptotics): introduce is_O_with (#1857)

* refactor(analysis/asymptotics): introduce `is_O_with`

I use it to factor out common parts of the proofs of facts about
`is_O` and `is_o`. It can also be used with `principal s` filter to
operate with `∀ x ∈ s, ∥f x∥ ≤ C * ∥g x∥` is a manner similar to `is_O`.

* lint

* Fix compile

* Drop `(s)mul_same` lemmas.

It's easy to use `(s)mul_is_O (is_O_refl _ _)` or `(is_O_refl _
_).mul_is_o _` instead

* docs: say explicitly that `is_O` is better than `is_O_with`

Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

src/analysis/calculus/deriv.lean

@@ -252,7 +252,7 @@ lemma has_deriv_within_at.union (hs : has_deriv_within_at f f' s x) (ht : has_de
   has_deriv_within_at f f' (s ∪ t) x :=
 begin
   simp only [has_deriv_within_at, nhds_within_union],
-  exact is_o_join hs ht,
+  exact hs.join ht,
 end
 
 lemma has_deriv_within_at.nhds_within (h : has_deriv_within_at f f' s x)
@@ -957,38 +957,35 @@ begin
   have : is_o (λ (h : 𝕜), h^2 * (1 + h)⁻¹) (λ (h : 𝕜), h * 1) (𝓝 0),
   { have : tendsto (λ (h : 𝕜), (1 + h)⁻¹) (𝓝 0) (𝓝 (1 + 0)⁻¹) :=
       ((tendsto_const_nhds).add tendsto_id).inv' (by norm_num),
-    exact is_o_mul_right (is_o_pow_id (by norm_num)) (is_O_one_of_tendsto this) },
-  apply (is_o_congr _ _).2 this,
-  { have : metric.ball (0 : 𝕜) (∥(1:𝕜)∥) ∈ 𝓝 (0 : 𝕜),
-    { apply mem_nhds_sets metric.is_open_ball,
-      simp [zero_lt_one] },
+    exact is_o.mul_is_O (is_o_pow_id one_lt_two) (is_O_one_of_tendsto _ this) },
+  apply this.congr' _ _,
+  { have : metric.ball (0 : 𝕜) 1 ∈ 𝓝 (0 : 𝕜),
+      from metric.ball_mem_nhds 0 zero_lt_one,
     filter_upwards [this],
     assume h hx,
     have : 0 < ∥1 + h∥ := calc
-      0 < ∥(1:𝕜)∥ - ∥-h∥ : by rwa [norm_neg, sub_pos, ← dist_zero_right h]
+      0 < ∥(1:𝕜)∥ - ∥-h∥ : by rwa [norm_neg, sub_pos, ← dist_zero_right h, normed_field.norm_one]
       ... ≤ ∥1 - -h∥ : norm_sub_norm_le _ _
       ... = ∥1 + h∥ : by simp,
     have : 1 + h ≠ 0 := (norm_pos_iff (1 + h)).mp this,
-    calc (1 + h)⁻¹ - 1⁻¹ - h * -1 =
-      (1+h)⁻¹ - ((1+h) * (1+h)⁻¹) + h * ((1+h) * (1+h)⁻¹) :
-        by { simp only [mul_inv_cancel this], simp }
-      ... = h^2 * (1+h)⁻¹ : by { generalize : (1+h)⁻¹ = y, ring } },
-  { convert univ_mem_sets, simp }
+    simp only [mem_set_of_eq, smul_eq_mul, inv_one],
+    field_simp [this, -add_comm],
+    ring },
+  { exact univ_mem_sets' mul_one }
 end
 
 theorem has_deriv_at_inv (x_ne_zero : x ≠ 0) :
   has_deriv_at (λy, y⁻¹) (-(x^2)⁻¹) x :=
 begin
   have A : has_deriv_at (λy, y⁻¹) (-1) (x⁻¹ * x : 𝕜),
-    by { simp [inv_mul_cancel x_ne_zero, has_deriv_at_inv_one] },
+    by { simp only [inv_mul_cancel x_ne_zero, has_deriv_at_inv_one] },
   have B : has_deriv_at (λy, x⁻¹ * y) (x⁻¹) x,
-    by { convert ((has_deriv_at_const x (x⁻¹)).mul (has_deriv_at_id x)), simp },
-  convert (has_deriv_at_const _ (x⁻¹)).mul (A.comp x B : _),
+    by simpa only [mul_one] using (has_deriv_at_id x).const_mul x⁻¹,
+  convert (A.comp x B : _).const_mul x⁻¹,
   { ext y,
-    have : x⁻¹ * (y⁻¹ * x) = y⁻¹,
-      by rw [← mul_assoc, mul_comm, ← mul_assoc, mul_inv_cancel x_ne_zero, one_mul],
-    simp [mul_inv', this] },
-  { simp [pow_two, mul_inv'] }
+    rw [function.comp_apply, mul_inv', inv_inv', mul_comm, mul_assoc, mul_inv_cancel x_ne_zero,
+      mul_one] },
+  { rw [pow_two, mul_inv', smul_eq_mul, mul_neg_one, neg_mul_eq_mul_neg] }
 end
 
 theorem has_deriv_within_at_inv (x_ne_zero : x ≠ 0) (s : set 𝕜) :

src/analysis/calculus/fderiv.lean

@@ -164,25 +164,22 @@ theorem has_fderiv_within_at.lim (h : has_fderiv_within_at f f' s x) {α : Type*
   (cdlim : tendsto (λ n, c n • d n) l (𝓝 v)) :
   tendsto (λn, c n • (f (x + d n) - f x)) l (𝓝 (f' v)) :=
 begin
-  have at_top_is_finer : l ≤ comap (λ n, x + d n) (nhds_within x s),
+  have tendsto_arg : tendsto (λ n, x + d n) l (nhds_within x s),
   { conv in (nhds_within x s) { rw ← add_zero x },
-    rw [← tendsto_iff_comap, nhds_within, tendsto_inf],
+    rw [nhds_within, tendsto_inf],
     split,
     { apply tendsto_const_nhds.add (tangent_cone_at.lim_zero l clim cdlim) },
     { rwa tendsto_principal } },
   have : is_o (λ y, f y - f x - f' (y - x)) (λ y, y - x) (nhds_within x s) := h,
-  have : is_o (λ n, f (x + d n) - f x - f' ((x + d n) - x)) (λ n, (x + d n)  - x)
-    ((nhds_within x s).comap (λn, x+ d n)) := is_o.comp this _,
-  have : is_o (λ n, f (x + d n) - f x - f' (d n)) d
-    ((nhds_within x s).comap (λn, x + d n)) := by simpa,
-  have : is_o (λn, f (x + d n) - f x - f' (d n)) d l :=
-    is_o.mono at_top_is_finer this,
+  have : is_o (λ n, f (x + d n) - f x - f' ((x + d n) - x)) (λ n, (x + d n)  - x) l :=
+    this.comp_tendsto tendsto_arg,
+  have : is_o (λ n, f (x + d n) - f x - f' (d n)) d l := by simpa only [add_sub_cancel'],
   have : is_o (λn, c n • (f (x + d n) - f x - f' (d n))) (λn, c n • d n) l :=
-    is_o_smul this,
+    (is_O_refl c l).smul_is_o this,
   have : is_o (λn, c n • (f (x + d n) - f x - f' (d n))) (λn, (1:ℝ)) l :=
-    this.trans_is_O (is_O_one_of_tendsto cdlim),
+    this.trans_is_O (is_O_one_of_tendsto ℝ cdlim),
   have L1 : tendsto (λn, c n • (f (x + d n) - f x - f' (d n))) l (𝓝 0) :=
-    is_o_one_iff.1 this,
+    (is_o_one_iff ℝ).1 this,
   have L2 : tendsto (λn, f' (c n • d n)) l (𝓝 (f' v)) :=
     tendsto.comp f'.cont.continuous_at cdlim,
   have L3 : tendsto (λn, (c n • (f (x + d n) - f x - f' (d n)) +  f' (c n • d n)))
@@ -254,22 +251,22 @@ theorem has_fderiv_at_iff_is_o_nhds_zero : has_fderiv_at f f' x ↔
 begin
   split,
   { assume H,
-    have : 𝓝 0 ≤ comap (λ (z : E), z + x) (𝓝 (0 + x)),
-    { refine tendsto_iff_comap.mp _,
-      exact (continuous_id.add continuous_const).tendsto _ },
-    apply is_o.mono this,
-    convert is_o.comp H (λz, z + x) ; { try {ext}, simp } },
+    have : tendsto (λ (z : E), z + x) (𝓝 0) (𝓝 (0 + x)),
+      from tendsto_id.add tendsto_const_nhds,
+    rw [zero_add] at this,
+    refine (H.comp_tendsto this).congr _ _;
+      intro z; simp only [function.comp, add_sub_cancel', add_comm z] },
   { assume H,
-    have : 𝓝 x ≤ comap (λ (z : E), z - x) (𝓝 (x - x)),
-    { refine tendsto_iff_comap.mp _,
-      exact (continuous_id.add continuous_const).tendsto _ },
-    apply is_o.mono this,
-    convert is_o.comp H (λz, z - x) ; { try {ext}, simp } }
+    have : tendsto (λ (z : E), z - x) (𝓝 x) (𝓝 (x - x)),
+      from tendsto_id.sub tendsto_const_nhds,
+    rw [sub_self] at this,
+    refine (H.comp_tendsto this).congr _ _;
+      intro z; simp only [function.comp, add_sub_cancel'_right] }
 end
 
 theorem has_fderiv_at_filter.mono (h : has_fderiv_at_filter f f' x L₂) (hst : L₁ ≤ L₂) :
   has_fderiv_at_filter f f' x L₁ :=
-is_o.mono hst h
+h.mono hst
 
 theorem has_fderiv_within_at.mono (h : has_fderiv_within_at f f' t x) (hst : s ⊆ t) :
   has_fderiv_within_at f f' s x :=
@@ -327,7 +324,7 @@ lemma has_fderiv_within_at.union (hs : has_fderiv_within_at f f' s x) (ht : has_
   has_fderiv_within_at f f' (s ∪ t) x :=
 begin
   simp only [has_fderiv_within_at, nhds_within_union],
-  exact is_o_join hs ht,
+  exact hs.join ht,
 end
 
 lemma has_fderiv_within_at.nhds_within (h : has_fderiv_within_at f f' s x)
@@ -370,7 +367,7 @@ lemma has_fderiv_within_at_of_not_mem_closure (h : x ∉ closure s) :
   has_fderiv_within_at f f' s x :=
 begin
   simp [mem_closure_iff_nhds_within_ne_bot] at h,
-  simp [has_fderiv_within_at, has_fderiv_at_filter, h, is_o]
+  simp [has_fderiv_within_at, has_fderiv_at_filter, h, is_o, is_O_with],
 end
 
 lemma differentiable_within_at.mono (h : differentiable_within_at 𝕜 f t x) (st : s ⊆ t) :
@@ -1008,7 +1005,7 @@ lemma fderiv_sub
 
 theorem has_fderiv_at_filter.is_O_sub (h : has_fderiv_at_filter f f' x L) :
 is_O (λ x', f x' - f x) (λ x', x' - x) L :=
-h.to_is_O.congr_of_sub.2 (f'.is_O_sub _ _)
+h.is_O.congr_of_sub.2 (f'.is_O_sub _ _)
 
 theorem has_fderiv_at_filter.sub_const
   (hf : has_fderiv_at_filter f f' x L) (c : F) :
@@ -1165,23 +1162,18 @@ begin
   rcases h.bound with ⟨C, Cpos, hC⟩,
   have A : asymptotics.is_O (λx : E × F, b (x.1 - p.1, x.2 - p.2))
     (λx, ∥x - p∥ * ∥x - p∥) (𝓝 p) :=
-  ⟨C, Cpos, filter.univ_mem_sets' (λx, begin
+  ⟨C, filter.univ_mem_sets' (λx, begin
     simp only [mem_set_of_eq, norm_mul, norm_norm],
     calc ∥b (x.1 - p.1, x.2 - p.2)∥ ≤ C * ∥x.1 - p.1∥ * ∥x.2 - p.2∥ : hC _ _
     ... ≤ C * ∥x-p∥ * ∥x-p∥ : by apply_rules [mul_le_mul, le_max_left, le_max_right, norm_nonneg,
       le_of_lt Cpos, le_refl, mul_nonneg, norm_nonneg, norm_nonneg]
     ... = C * (∥x-p∥ * ∥x-p∥) : mul_assoc _ _ _ end)⟩,
   have B : asymptotics.is_o (λ (x : E × F), ∥x - p∥ * ∥x - p∥)
     (λx, 1 * ∥x - p∥) (𝓝 p),
-  { apply asymptotics.is_o_mul_right _ (asymptotics.is_O_refl _ _),
-    rw [asymptotics.is_o_iff_tendsto],
-    { simp only [div_one],
-      have : 0 = ∥p - p∥, by simp,
-      rw this,
-      have : continuous (λx, ∥x-p∥) :=
-        continuous_norm.comp (continuous_id.sub continuous_const),
-      exact this.tendsto p },
-    simp only [forall_prop_of_false, not_false_iff, one_ne_zero, forall_true_iff] },
+  { refine asymptotics.is_o.mul_is_O (asymptotics.is_o.norm_left _) (asymptotics.is_O_refl _ _),
+    apply (asymptotics.is_o_one_iff ℝ).2,
+    rw [← sub_self p],
+    exact tendsto_id.sub tendsto_const_nhds },
   simp only [one_mul, asymptotics.is_o_norm_right] at B,
   exact A.trans_is_o B
 end
@@ -1305,8 +1297,8 @@ theorem has_fderiv_at_filter.comp {g : F → G} {g' : F →L[𝕜] G}
   (hf : has_fderiv_at_filter f f' x L) :
   has_fderiv_at_filter (g ∘ f) (g'.comp f') x L :=
 let eq₁ := (g'.is_O_comp _ _).trans_is_o hf in
-let eq₂ := ((hg.comp f).mono le_comap_map).trans_is_O hf.is_O_sub in
-by { refine eq₂.tri (eq₁.congr_left (λ x', _)), simp }
+let eq₂ := (hg.comp_tendsto tendsto_map).trans_is_O hf.is_O_sub in
+by { refine eq₂.triangle (eq₁.congr_left (λ x', _)), simp }
 
 /- A readable version of the previous theorem,
    a general form of the chain rule. -/
@@ -1318,7 +1310,7 @@ example {g : F → G} {g' : F →L[𝕜] G}
 begin
   unfold has_fderiv_at_filter at hg,
   have : is_o (λ x', g (f x') - g (f x) - g' (f x' - f x)) (λ x', f x' - f x) L,
-    from (hg.comp f).mono le_comap_map,
+    from hg.comp_tendsto (le_refl _),
   have eq₁ : is_o (λ x', g (f x') - g (f x) - g' (f x' - f x)) (λ x', x' - x) L,
     from this.trans_is_O hf.is_O_sub,
   have eq₂ : is_o (λ x', f x' - f x - f' (x' - x)) (λ x', x' - x) L,
@@ -1330,7 +1322,7 @@ begin
     from this.trans_is_o eq₂,
   have eq₃ : is_o (λ x', g' (f x' - f x) - (g' (f' (x' - x)))) (λ x', x' - x) L,
     by { refine this.congr_left _, simp},
-  exact eq₁.tri eq₃
+  exact eq₁.triangle eq₃
 end
 
 theorem has_fderiv_within_at.comp {g : F → G} {g' : F →L[𝕜] G} {t : set F}

src/analysis/calculus/mean_value.lean

@@ -83,7 +83,7 @@ begin
     have : is_o (λ x, h x) (λ x, x - k) (nhds_within k (Icc 0 1)) :=
       (hf k k_mem_K.1).has_deriv_within_at,
     have : {x | ∥h x∥ ≤ (D-C) * ∥x-k∥} ∈ nhds_within k (Icc 0 1) :=
-      this (D-C) (sub_pos_of_lt hD),
+      this (sub_pos_of_lt hD),
     rcases mem_nhds_within.1 this with ⟨s, s_open, ks, hs⟩,
     rcases is_open_iff.1 s_open k ks with ⟨ε, εpos, hε⟩,
     change 0 < ε at εpos,

src/analysis/complex/exponential.lean

@@ -48,9 +48,8 @@ lemma has_deriv_at_exp (x : ℂ) : has_deriv_at exp (exp x) x :=
 begin
   rw has_deriv_at_iff_is_o_nhds_zero,
   have : (1 : ℕ) < 2 := by norm_num,
-  refine is_O.trans_is_o (is_O_iff.2 ⟨∥exp x∥, _⟩) (is_o_pow_id this),
-  have : metric.ball (0 : ℂ) 1 ∈ nhds (0 : ℂ) :=
-    mem_nhds_sets metric.is_open_ball (by simp [zero_lt_one]),
+  refine is_O.trans_is_o ⟨∥exp x∥, _⟩ (is_o_pow_id this),
+  have : metric.ball (0 : ℂ) 1 ∈ nhds (0 : ℂ) := metric.ball_mem_nhds 0 zero_lt_one,
   apply filter.mem_sets_of_superset this (λz hz, _),
   simp only [metric.mem_ball, dist_zero_right] at hz,
   simp only [exp_zero, mul_one, one_mul, add_comm, normed_field.norm_pow,

src/analysis/normed_space/bounded_linear_maps.lean

@@ -134,11 +134,11 @@ open asymptotics filter
 theorem is_O_id {f : E → F} (h : is_bounded_linear_map 𝕜 f) (l : filter E) :
   is_O f (λ x, x) l :=
 let ⟨M, hMp, hM⟩ := h.bound in
-⟨M, hMp, mem_sets_of_superset univ_mem_sets (λ x _, hM x)⟩
+⟨M, mem_sets_of_superset univ_mem_sets (λ x _, hM x)⟩
 
 theorem is_O_comp {E : Type*} {g : F → G} (hg : is_bounded_linear_map 𝕜 g)
   {f : E → F} (l : filter E) : is_O (λ x', g (f x')) f l :=
-((hg.is_O_id ⊤).comp _).mono (map_le_iff_le_comap.mp lattice.le_top)
+(hg.is_O_id ⊤).comp_tendsto lattice.le_top
 
 theorem is_O_sub {f : E → F} (h : is_bounded_linear_map 𝕜 f)
   (l : filter E) (x : E) : is_O (λ x', f (x' - x)) (λ x', x' - x) l :=

src/analysis/normed_space/operator_norm.lean

@@ -158,16 +158,15 @@ section
 open asymptotics filter
 
 theorem is_O_id (l : filter E) : is_O f (λ x, x) l :=
-let ⟨M, hMp, hM⟩ := f.bound in
-⟨M, hMp, mem_sets_of_superset univ_mem_sets (λ x _, hM x)⟩
+let ⟨M, hMp, hM⟩ := f.bound in is_O_of_le' l hM
 
 theorem is_O_comp {E : Type*} (g : F →L[𝕜] G) (f : E → F) (l : filter E) :
   is_O (λ x', g (f x')) f l :=
-((g.is_O_id ⊤).comp _).mono (map_le_iff_le_comap.mp lattice.le_top)
+(g.is_O_id ⊤).comp_tendsto lattice.le_top
 
 theorem is_O_sub (f : E →L[𝕜] F) (l : filter E) (x : E) :
   is_O (λ x', f (x' - x)) (λ x', x' - x) l :=
-is_O_comp f _ l
+f.is_O_comp _ l
 
 end