feat(measure_theory/interval_integral): more versions of FTC-1 (#3709)

Left/right derivative, strict derivative, differentiability in both endpoints.

Other changes:

* rename `filter.tendsto_le_left` and `filter.tendsto_le_right` to `filter.tendsto.mono_left` and `filter.tendsto.mono_right`, swap arguments;
* rename `order_top.tendsto_at_top` to `order_top.tendsto_at_top_nhds`;
* introduce `tendsto_Ixx_class` instead of `is_interval_generated`.



Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

src/analysis/calculus/extend_deriv.lean

@@ -125,7 +125,7 @@ begin
   have t_diff' : tendsto (λx, fderiv ℝ f x) (𝓝[t] a) (𝓝 (smul_right 1 e)),
   { simp [deriv_fderiv.symm],
     refine tendsto.comp is_bounded_bilinear_map_smul_right.continuous_right.continuous_at _,
-    exact tendsto_le_left (nhds_within_mono _ Ioo_subset_Ioi_self) f_lim' },
+    exact tendsto_nhds_within_mono_left Ioo_subset_Ioi_self f_lim' },
   -- now we can apply `has_fderiv_at_boundary_of_differentiable`
   have : has_deriv_within_at f e (Icc a b) a,
   { rw [has_deriv_within_at_iff_has_fderiv_within_at, ← t_closure],
@@ -162,7 +162,7 @@ begin
   have t_diff' : tendsto (λx, fderiv ℝ f x) (𝓝[t] a) (𝓝 (smul_right 1 e)),
   { simp [deriv_fderiv.symm],
     refine tendsto.comp is_bounded_bilinear_map_smul_right.continuous_right.continuous_at _,
-    exact tendsto_le_left (nhds_within_mono _ Ioo_subset_Iio_self) f_lim' },
+    exact tendsto_nhds_within_mono_left Ioo_subset_Iio_self f_lim' },
   -- now we can apply `has_fderiv_at_boundary_of_differentiable`
   have : has_deriv_within_at f e (Icc b a) a,
   { rw [has_deriv_within_at_iff_has_fderiv_within_at, ← t_closure],

src/analysis/calculus/fderiv.lean

@@ -537,7 +537,7 @@ theorem has_fderiv_at_filter.tendsto_nhds
   tendsto f L (𝓝 (f x)) :=
 begin
   have : tendsto (λ x', f x' - f x) L (𝓝 0),
-  { refine h.is_O_sub.trans_tendsto (tendsto_le_left hL _),
+  { refine h.is_O_sub.trans_tendsto (tendsto.mono_left _ hL),
     rw ← sub_self x, exact tendsto_id.sub tendsto_const_nhds },
   have := tendsto.add this tendsto_const_nhds,
   rw zero_add (f x) at this,
@@ -1053,7 +1053,7 @@ protected lemma has_fderiv_within_at.iterate {f : E → E} {f' : E →L[𝕜] E}
 begin
   refine hf.iterate _ hx n,
   convert tendsto_inf.2 ⟨hf.continuous_within_at, _⟩,
-  exacts [hx.symm, tendsto_le_left inf_le_right (tendsto_principal_principal.2 hs)]
+  exacts [hx.symm, (tendsto_principal_principal.2 hs).mono_left inf_le_right]
 end
 
 protected lemma has_strict_fderiv_at.iterate {f : E → E} {f' : E →L[𝕜] E}

src/analysis/calculus/tangent_cone.lean

@@ -117,8 +117,7 @@ begin
   refine ⟨c, d, _, ctop, clim⟩,
   suffices : tendsto (λ n, x + d n) at_top (𝓝[t] x),
     from tendsto_principal.1 (tendsto_inf.1 this).2,
-  apply tendsto_le_right h,
-  refine tendsto_inf.2 ⟨_, tendsto_principal.2 ds⟩,
+  refine (tendsto_inf.2 ⟨_, tendsto_principal.2 ds⟩).mono_right h,
   simpa only [add_zero] using tendsto_const_nhds.add (tangent_cone_at.lim_zero at_top ctop clim)
 end
 
@@ -246,8 +245,14 @@ end
 end tangent_cone
 
 section unique_diff
-/- This section is devoted to properties of the predicates `unique_diff_within_at` and
-`unique_diff_on`. -/
+/-!
+### Properties of `unique_diff_within_at` and `unique_diff_on`
+
+This section is devoted to properties of the predicates `unique_diff_within_at` and `unique_diff_on`. -/
+
+lemma unique_diff_on.unique_diff_within_at {s : set E} {x} (hs : unique_diff_on 𝕜 s) (h : x ∈ s) :
+  unique_diff_within_at 𝕜 s x :=
+hs x h
 
 lemma unique_diff_within_at_univ : unique_diff_within_at 𝕜 univ x :=
 by { rw [unique_diff_within_at, tangent_cone_univ], simp }

src/analysis/specific_limits.lean

@@ -116,7 +116,7 @@ end
 
 lemma tendsto_inv_at_top_zero [discrete_linear_ordered_field α] [topological_space α]
   [order_topology α] : tendsto (λr:α, r⁻¹) at_top (𝓝 0) :=
-tendsto_le_right inf_le_left tendsto_inv_at_top_zero'
+tendsto_inv_at_top_zero'.mono_right inf_le_left 
 
 lemma summable_of_absolute_convergence_real {f : ℕ → ℝ} :
   (∃r, tendsto (λn, (∑ i in range n, abs (f i))) at_top (𝓝 r)) → summable f

src/measure_theory/borel_space.lean

@@ -205,6 +205,14 @@ lemma is_measurable_Ici : is_measurable (Ici a) := is_closed_Ici.is_measurable
 lemma is_measurable_Iic : is_measurable (Iic a) := is_closed_Iic.is_measurable
 lemma is_measurable_Icc : is_measurable (Icc a b) := is_closed_Icc.is_measurable
 
+instance nhds_within_Ici_is_measurably_generated :
+  (𝓝[Ici b] a).is_measurably_generated :=
+is_measurable_Ici.nhds_within_is_measurably_generated _
+
+instance nhds_within_Iic_is_measurably_generated :
+  (𝓝[Iic b] a).is_measurably_generated :=
+is_measurable_Iic.nhds_within_is_measurably_generated _
+
 instance at_top_is_measurably_generated : (filter.at_top : filter α).is_measurably_generated :=
 @filter.infi_is_measurably_generated _ _ _ _ $
   λ a, (is_measurable_Ici : is_measurable (Ici a)).principal_is_measurably_generated
@@ -224,6 +232,14 @@ lemma is_measurable_Ioo : is_measurable (Ioo a b) := is_open_Ioo.is_measurable
 lemma is_measurable_Ioc : is_measurable (Ioc a b) := is_measurable_Ioi.inter is_measurable_Iic
 lemma is_measurable_Ico : is_measurable (Ico a b) := is_measurable_Ici.inter is_measurable_Iio
 
+instance nhds_within_Ioi_is_measurably_generated :
+  (𝓝[Ioi b] a).is_measurably_generated :=
+is_measurable_Ioi.nhds_within_is_measurably_generated _
+
+instance nhds_within_Iio_is_measurably_generated :
+  (𝓝[Iio b] a).is_measurably_generated :=
+is_measurable_Iio.nhds_within_is_measurably_generated _
+
 end order_closed_topology
 
 lemma is_measurable_interval [decidable_linear_order α] [order_closed_topology α] {a b : α} :