[Merged by Bors] - feat(measure_theory/interval_integral): FTC-2

src/analysis/ODE/gronwall.lean

@@ -133,7 +133,7 @@ end
 `∀ x ∈ [a, b), ∥f' x∥ ≤ K * ∥f x∥ + ε`, then `∥f x∥` is bounded by `gronwall_bound δ K ε (x - a)`
 on `[a, b]`. -/
 theorem norm_le_gronwall_bound_of_norm_deriv_right_le {f f' : ℝ → E} {δ K ε : ℝ} {a b : ℝ}
-  (hf : continuous_on f (Icc a b)) (hf' : ∀ x ∈ Ico a b, has_deriv_within_at f (f' x) (Ioi x) x)
+  (hf : continuous_on f (Icc a b)) (hf' : ∀ x ∈ Ico a b, has_deriv_within_at f (f' x) (Ici x) x)
   (ha : ∥f a∥ ≤ δ) (bound : ∀ x ∈ Ico a b, ∥f' x∥ ≤ K * ∥f x∥ + ε) :
   ∀ x ∈ Icc a b, ∥f x∥ ≤ gronwall_bound δ K ε (x - a) :=
 le_gronwall_bound_of_liminf_deriv_right_le (continuous_norm.comp_continuous_on hf)
@@ -149,18 +149,18 @@ theorem dist_le_of_approx_trajectories_ODE_of_mem_set {v : ℝ → E → E} {s :
   {K : ℝ} (hv : ∀ t, ∀ x y ∈ s t, dist (v t x) (v t y) ≤ K * dist x y)
   {f g f' g' : ℝ → E} {a b : ℝ} {εf εg δ : ℝ}
   (hf : continuous_on f (Icc a b))
-  (hf' : ∀ t ∈ Ico a b, has_deriv_within_at f (f' t) (Ioi t) t)
+  (hf' : ∀ t ∈ Ico a b, has_deriv_within_at f (f' t) (Ici t) t)
   (f_bound : ∀ t ∈ Ico a b, dist (f' t) (v t (f t)) ≤ εf)
   (hfs : ∀ t ∈ Ico a b, f t ∈ s t)
   (hg : continuous_on g (Icc a b))
-  (hg' : ∀ t ∈ Ico a b, has_deriv_within_at g (g' t) (Ioi t) t)
+  (hg' : ∀ t ∈ Ico a b, has_deriv_within_at g (g' t) (Ici t) t)
   (g_bound : ∀ t ∈ Ico a b, dist (g' t) (v t (g t)) ≤ εg)
   (hgs : ∀ t ∈ Ico a b, g t ∈ s t)
   (ha : dist (f a) (g a) ≤ δ) :
   ∀ t ∈ Icc a b, dist (f t) (g t) ≤ gronwall_bound δ K (εf + εg) (t - a) :=
 begin
   simp only [dist_eq_norm] at ha ⊢,
-  have h_deriv : ∀ t ∈ Ico a b, has_deriv_within_at (λ t, f t - g t) (f' t - g' t) (Ioi t) t,
+  have h_deriv : ∀ t ∈ Ico a b, has_deriv_within_at (λ t, f t - g t) (f' t - g' t) (Ici t) t,
     from λ t ht, (hf' t ht).sub (hg' t ht),
   apply norm_le_gronwall_bound_of_norm_deriv_right_le (hf.sub hg) h_deriv ha,
   assume t ht,
@@ -181,10 +181,10 @@ theorem dist_le_of_approx_trajectories_ODE {v : ℝ → E → E}
   {K : ℝ≥0} (hv : ∀ t, lipschitz_with K (v t))
   {f g f' g' : ℝ → E} {a b : ℝ} {εf εg δ : ℝ}
   (hf : continuous_on f (Icc a b))
-  (hf' : ∀ t ∈ Ico a b, has_deriv_within_at f (f' t) (Ioi t) t)
+  (hf' : ∀ t ∈ Ico a b, has_deriv_within_at f (f' t) (Ici t) t)
   (f_bound : ∀ t ∈ Ico a b, dist (f' t) (v t (f t)) ≤ εf)
   (hg : continuous_on g (Icc a b))
-  (hg' : ∀ t ∈ Ico a b, has_deriv_within_at g (g' t) (Ioi t) t)
+  (hg' : ∀ t ∈ Ico a b, has_deriv_within_at g (g' t) (Ici t) t)
   (g_bound : ∀ t ∈ Ico a b, dist (g' t) (v t (g t)) ≤ εg)
   (ha : dist (f a) (g a) ≤ δ) :
   ∀ t ∈ Icc a b, dist (f t) (g t) ≤ gronwall_bound δ K (εf + εg) (t - a) :=
@@ -202,10 +202,10 @@ theorem dist_le_of_trajectories_ODE_of_mem_set {v : ℝ → E → E} {s : ℝ 
   {K : ℝ} (hv : ∀ t, ∀ x y ∈ s t, dist (v t x) (v t y) ≤ K * dist x y)
   {f g : ℝ → E} {a b : ℝ} {δ : ℝ}
   (hf : continuous_on f (Icc a b))
-  (hf' : ∀ t ∈ Ico a b, has_deriv_within_at f (v t (f t)) (Ioi t) t)
+  (hf' : ∀ t ∈ Ico a b, has_deriv_within_at f (v t (f t)) (Ici t) t)
   (hfs : ∀ t ∈ Ico a b, f t ∈ s t)
   (hg : continuous_on g (Icc a b))
-  (hg' : ∀ t ∈ Ico a b, has_deriv_within_at g (v t (g t)) (Ioi t) t)
+  (hg' : ∀ t ∈ Ico a b, has_deriv_within_at g (v t (g t)) (Ici t) t)
   (hgs : ∀ t ∈ Ico a b, g t ∈ s t)
   (ha : dist (f a) (g a) ≤ δ) :
   ∀ t ∈ Icc a b, dist (f t) (g t) ≤ δ * exp (K * (t - a)) :=
@@ -229,9 +229,9 @@ theorem dist_le_of_trajectories_ODE {v : ℝ → E → E}
   {K : ℝ≥0} (hv : ∀ t, lipschitz_with K (v t))
   {f g : ℝ → E} {a b : ℝ} {δ : ℝ}
   (hf : continuous_on f (Icc a b))
-  (hf' : ∀ t ∈ Ico a b, has_deriv_within_at f (v t (f t)) (Ioi t) t)
+  (hf' : ∀ t ∈ Ico a b, has_deriv_within_at f (v t (f t)) (Ici t) t)
   (hg : continuous_on g (Icc a b))
-  (hg' : ∀ t ∈ Ico a b, has_deriv_within_at g (v t (g t)) (Ioi t) t)
+  (hg' : ∀ t ∈ Ico a b, has_deriv_within_at g (v t (g t)) (Ici t) t)
   (ha : dist (f a) (g a) ≤ δ) :
   ∀ t ∈ Icc a b, dist (f t) (g t) ≤ δ * exp (K * (t - a)) :=
 have hfs : ∀ t ∈ Ico a b, f t ∈ (@univ E), from λ t ht, trivial,
@@ -245,10 +245,10 @@ theorem ODE_solution_unique_of_mem_set {v : ℝ → E → E} {s : ℝ → set E}
   {K : ℝ} (hv : ∀ t, ∀ x y ∈ s t, dist (v t x) (v t y) ≤ K * dist x y)
   {f g : ℝ → E} {a b : ℝ}
   (hf : continuous_on f (Icc a b))
-  (hf' : ∀ t ∈ Ico a b, has_deriv_within_at f (v t (f t)) (Ioi t) t)
+  (hf' : ∀ t ∈ Ico a b, has_deriv_within_at f (v t (f t)) (Ici t) t)
   (hfs : ∀ t ∈ Ico a b, f t ∈ s t)
   (hg : continuous_on g (Icc a b))
-  (hg' : ∀ t ∈ Ico a b, has_deriv_within_at g (v t (g t)) (Ioi t) t)
+  (hg' : ∀ t ∈ Ico a b, has_deriv_within_at g (v t (g t)) (Ici t) t)
   (hgs : ∀ t ∈ Ico a b, g t ∈ s t)
   (ha : f a = g a) :
   ∀ t ∈ Icc a b, f t = g t :=
@@ -265,9 +265,9 @@ theorem ODE_solution_unique {v : ℝ → E → E}
   {K : ℝ≥0} (hv : ∀ t, lipschitz_with K (v t))
   {f g : ℝ → E} {a b : ℝ}
   (hf : continuous_on f (Icc a b))
-  (hf' : ∀ t ∈ Ico a b, has_deriv_within_at f (v t (f t)) (Ioi t) t)
+  (hf' : ∀ t ∈ Ico a b, has_deriv_within_at f (v t (f t)) (Ici t) t)
   (hg : continuous_on g (Icc a b))
-  (hg' : ∀ t ∈ Ico a b, has_deriv_within_at g (v t (g t)) (Ioi t) t)
+  (hg' : ∀ t ∈ Ico a b, has_deriv_within_at g (v t (g t)) (Ici t) t)
   (ha : f a = g a) :
   ∀ t ∈ Icc a b, f t = g t :=
 have hfs : ∀ t ∈ Ico a b, f t ∈ (@univ E), from λ t ht, trivial,

src/analysis/calculus/deriv.lean

@@ -242,27 +242,45 @@ begin
   rw [smul_sub, ← mul_smul, inv_mul_cancel (sub_ne_zero.2 hz), one_smul]
 end
 
-lemma has_deriv_within_at_iff_tendsto_slope {x : 𝕜} {s : set 𝕜} :
+lemma has_deriv_within_at_iff_tendsto_slope :
   has_deriv_within_at f f' s x ↔
     tendsto (λ y, (y - x)⁻¹ • (f y - f x)) (𝓝[s \ {x}] x) (𝓝 f') :=
 begin
   simp only [has_deriv_within_at, nhds_within, diff_eq, inf_assoc.symm, inf_principal.symm],
   exact has_deriv_at_filter_iff_tendsto_slope
 end
 
-lemma has_deriv_within_at_iff_tendsto_slope' {x : 𝕜} {s : set 𝕜} (hs : x ∉ s) :
+lemma has_deriv_within_at_iff_tendsto_slope' (hs : x ∉ s) :
   has_deriv_within_at f f' s x ↔
     tendsto (λ y, (y - x)⁻¹ • (f y - f x)) (𝓝[s] x) (𝓝 f') :=
 begin
   convert ← has_deriv_within_at_iff_tendsto_slope,
   exact diff_singleton_eq_self hs
 end
 
-lemma has_deriv_at_iff_tendsto_slope {x : 𝕜} :
+lemma has_deriv_at_iff_tendsto_slope :
   has_deriv_at f f' x ↔
     tendsto (λ y, (y - x)⁻¹ • (f y - f x)) (𝓝[{x}ᶜ] x) (𝓝 f') :=
 has_deriv_at_filter_iff_tendsto_slope
 
+@[simp] lemma has_deriv_within_at_diff_singleton :
+  has_deriv_within_at f f' (s \ {x}) x ↔ has_deriv_within_at f f' s x :=
+by simp only [has_deriv_within_at_iff_tendsto_slope, sdiff_idem_right]
+
+@[simp] lemma has_deriv_within_at_Ioi_iff_Ici [partial_order 𝕜] :
+  has_deriv_within_at f f' (Ioi x) x ↔ has_deriv_within_at f f' (Ici x) x :=
+by rw [← Ici_diff_left, has_deriv_within_at_diff_singleton]
+
+alias has_deriv_within_at_Ioi_iff_Ici ↔
+  has_deriv_within_at.Ici_of_Ioi has_deriv_within_at.Ioi_of_Ici
+
+@[simp] lemma has_deriv_within_at_Iio_iff_Iic [partial_order 𝕜] :
+  has_deriv_within_at f f' (Iio x) x ↔ has_deriv_within_at f f' (Iic x) x :=
+by rw [← Iic_diff_right, has_deriv_within_at_diff_singleton]
+
+alias has_deriv_within_at_Iio_iff_Iic ↔
+  has_deriv_within_at.Iic_of_Iio has_deriv_within_at.Iio_of_Iic
+
 theorem has_deriv_at_iff_is_o_nhds_zero : has_deriv_at f f' x ↔
   is_o (λh, f (x + h) - f x - h • f') (λh, h) (𝓝 0) :=
 has_fderiv_at_iff_is_o_nhds_zero
@@ -1727,9 +1745,9 @@ lemma has_deriv_within_at.limsup_slope_le' (hf : has_deriv_within_at f f' s x)
 (has_deriv_within_at_iff_tendsto_slope' hs).1 hf (mem_nhds_sets is_open_Iio hr)
 
 lemma has_deriv_within_at.liminf_right_slope_le
-  (hf : has_deriv_within_at f f' (Ioi x) x) (hr : f' < r) :
+  (hf : has_deriv_within_at f f' (Ici x) x) (hr : f' < r) :
   ∃ᶠ z in 𝓝[Ioi x] x, (z - x)⁻¹ * (f z - f x) < r :=
-(hf.limsup_slope_le' (lt_irrefl x) hr).frequently
+(hf.Ioi_of_Ici.limsup_slope_le' (lt_irrefl x) hr).frequently
 
 end real
 
@@ -1784,9 +1802,9 @@ In other words, the limit inferior of this ratio as `z` tends to `x+0`
 is less than or equal to `∥f'∥`. See also `has_deriv_within_at.limsup_norm_slope_le`
 for a stronger version using limit superior and any set `s`. -/
 lemma has_deriv_within_at.liminf_right_norm_slope_le
-  (hf : has_deriv_within_at f f' (Ioi x) x) (hr : ∥f'∥ < r) :
+  (hf : has_deriv_within_at f f' (Ici x) x) (hr : ∥f'∥ < r) :
   ∃ᶠ z in 𝓝[Ioi x] x, ∥z - x∥⁻¹ * ∥f z - f x∥ < r :=
-(hf.limsup_norm_slope_le hr).frequently
+(hf.Ioi_of_Ici.limsup_norm_slope_le hr).frequently
 
 /-- If `f` has derivative `f'` within `(x, +∞)` at `x`, then for any `r > ∥f'∥` the ratio
 `(∥f z∥ - ∥f x∥) / (z - x)` is frequently less than `r` as `z → x+0`.
@@ -1800,10 +1818,10 @@ See also
 * `has_deriv_within_at.liminf_right_norm_slope_le` for a stronger version using
   `∥f z - f x∥` instead of `∥f z∥ - ∥f x∥`. -/
 lemma has_deriv_within_at.liminf_right_slope_norm_le
-  (hf : has_deriv_within_at f f' (Ioi x) x) (hr : ∥f'∥ < r) :
+  (hf : has_deriv_within_at f f' (Ici x) x) (hr : ∥f'∥ < r) :
   ∃ᶠ z in 𝓝[Ioi x] x, (z - x)⁻¹ * (∥f z∥ - ∥f x∥) < r :=
 begin
-  have := (hf.limsup_slope_norm_le hr).frequently,
+  have := (hf.Ioi_of_Ici.limsup_slope_norm_le hr).frequently,
   refine this.mp (eventually.mono self_mem_nhds_within _),
   assume z hxz hz,
   rwa [real.norm_eq_abs, abs_of_pos (sub_pos_of_lt hxz)] at hz