simplify using #18844

src/analysis/special_functions/improper_integrals.lean

@@ -24,37 +24,29 @@ open_locale topology
 
 lemma integral_exp_neg_Ioi : ∫ (x : ℝ) in Ioi 0, exp (-x) = 1 :=
 begin
-  refine tendsto_nhds_unique (interval_integral_tendsto_integral_Ioi _ _ tendsto_id) _,
-  { simpa only [neg_mul, one_mul] using exp_neg_integrable_on_Ioi 0 zero_lt_one, },
-  { simpa only [interval_integral.integral_comp_neg, neg_zero, integral_exp, exp_zero,
-      tsub_zero] using tendsto.const_sub 1 tendsto_exp_neg_at_top_nhds_0, },
+  have h : ∀ (x : ℝ), x ∈ Ici (0:ℝ) → has_deriv_at (λ t, -exp (-t)) (exp (-x)) x,
+  { intros x hx, simpa using ((has_deriv_at_exp _).comp _ (has_deriv_at_neg x)).neg},
+  simpa only [neg_zero, zero_sub, neg_neg, exp_zero] using integral_Ioi_of_has_deriv_at_of_nonneg'
+    h (λ x _, (exp_pos _).le) (tendsto_exp_neg_at_top_nhds_0).neg,
 end
 
 /-- If `0 < c`, then `(λ t : ℝ, t ^ a)` is integrable on `(c, ∞)` for all `a < -1`. -/
 lemma integrable_on_Ioi_rpow_of_lt {a : ℝ} (ha : a < -1) {c : ℝ} (hc : 0 < c) :
   integrable_on (λ t : ℝ, t ^ a) (Ioi c) :=
 begin
-  refine integrable_on_Ioi_of_interval_integral_norm_bounded
-    (-c ^ (a + 1) / (a + 1)) c (λ i , _) tendsto_id _,
-  { dsimp only [id.def],
-    by_cases h : c ≤ i,
-    { rw ←interval_integrable_iff_integrable_Ioc_of_le h,
-      apply interval_integral.interval_integrable_rpow,
-      rw uIcc_of_le h,
-      exact or.inr (not_mem_Icc_of_lt hc) },
-    { rw Ioc_eq_empty (not_lt.mpr (not_le.mp h).le),
-      exact integrable_on_empty } },
-  refine (eventually_gt_at_top c).mp (eventually_of_forall (λ y hy, _)),
-  refine (le_of_eq _).trans (_ : ∫ x : ℝ in c..y, x ^ a ≤ _),
-  { refine interval_integral.integral_congr (λ x hx, _),
-    rw [id.def, uIcc_of_le hy.le] at hx,
-    dsimp only,
-    refine norm_of_nonneg (rpow_pos_of_pos (hc.trans_le hx.1) _).le },
-  { rw integral_rpow (or.inr ⟨ha.ne, not_mem_uIcc_of_lt hc $ hc.trans hy⟩),
-    refine div_le_div_of_nonpos_of_le _ _,
-    { rw [←sub_neg, sub_neg_eq_add] at ha, exact ha.le },
-    { rw sub_eq_add_neg,
-      refine le_add_of_nonneg_left (rpow_nonneg_of_nonneg (hc.trans hy).le _) } },
+  have hd : ∀ (x : ℝ) (hx : x ∈ Ici c), has_deriv_at (λ t, t ^ (a + 1) / (a + 1)) (x ^ a) x,
+  { intros x hx,
+    simp_rw div_eq_inv_mul,
+    have : x ^ a = (a + 1)⁻¹ * ((a + 1) * x ^ a),
+    { rw [←mul_assoc, inv_mul_cancel, one_mul], linarith },
+    rw this,
+    convert (has_deriv_at_rpow_const (or.inl (hc.trans_le hx).ne')).const_mul _,
+    abel },
+  have ht : tendsto (λ t, t ^ (a + 1) / (a + 1)) at_top (𝓝 0),
+  { rw ←zero_div,
+    apply tendsto.div_const,
+    simpa only [neg_neg] using tendsto_rpow_neg_at_top (by linarith : 0 < -(a + 1)) },
+  exact integrable_on_Ioi_deriv_of_nonneg' hd (λ t ht, rpow_nonneg_of_nonneg (hc.trans ht).le a) ht
 end
 
 lemma integral_Ioi_rpow_of_lt {a : ℝ} (ha : a < -1) {c : ℝ} (hc : 0 < c) :