feat(measure_theory/integral/interval_integral): one more FTC-2 (#9409)

src/measure_theory/integral/interval_integral.lean

@@ -164,7 +164,7 @@ integral, fundamental theorem of calculus, FTC-1, FTC-2, change of variables in
 
 noncomputable theory
 open topological_space (second_countable_topology)
-open measure_theory set classical filter
+open measure_theory set classical filter function
 
 open_locale classical topological_space filter ennreal big_operators
 
@@ -840,13 +840,13 @@ begin
     simp only [integrable_on_const, measure_lt_top, or_true]
 end
 
-lemma integral_eq_integral_of_support_subset {f : α → E} {a b} (h : function.support f ⊆ Ioc a b) :
+lemma integral_eq_integral_of_support_subset {f : α → E} {a b} (h : support f ⊆ Ioc a b) :
   ∫ x in a..b, f x ∂μ = ∫ x, f x ∂μ :=
 begin
   cases le_total a b with hab hab,
   { rw [integral_of_le hab, ← integral_indicator measurable_set_Ioc, indicator_eq_self.2 h];
     apply_instance },
-  { rw [Ioc_eq_empty hab.not_lt, subset_empty_iff, function.support_eq_empty_iff] at h,
+  { rw [Ioc_eq_empty hab.not_lt, subset_empty_iff, support_eq_empty_iff] at h,
     simp [h] }
 end
 
@@ -1120,7 +1120,7 @@ end
 
 lemma integral_pos_iff_support_of_nonneg_ae'
   (hf : 0 ≤ᵐ[μ.restrict (Ioc a b ∪ Ioc b a)] f) (hfi : interval_integrable f μ a b) :
-  0 < ∫ x in a..b, f x ∂μ ↔ a < b ∧ 0 < μ (function.support f ∩ Ioc a b) :=
+  0 < ∫ x in a..b, f x ∂μ ↔ a < b ∧ 0 < μ (support f ∩ Ioc a b) :=
 begin
   obtain hab | hab := le_total b a;
     simp only [Ioc_eq_empty hab.not_lt, empty_union, union_empty] at hf ⊢,
@@ -1136,7 +1136,7 @@ end
 
 lemma integral_pos_iff_support_of_nonneg_ae
   (hf : 0 ≤ᵐ[μ] f) (hfi : interval_integrable f μ a b) :
-  0 < ∫ x in a..b, f x ∂μ ↔ a < b ∧ 0 < μ (function.support f ∩ Ioc a b) :=
+  0 < ∫ x in a..b, f x ∂μ ↔ a < b ∧ 0 < μ (support f ∩ Ioc a b) :=
 integral_pos_iff_support_of_nonneg_ae' (ae_mono measure.restrict_le_self hf) hfi
 
 variable (hab : a ≤ b)
@@ -2197,6 +2197,28 @@ theorem integral_eq_sub_of_has_deriv_at
 integral_eq_sub_of_has_deriv_right (has_deriv_at.continuous_on hderiv)
   (λ x hx, (hderiv _ (mem_Icc_of_Ioo hx)).has_deriv_within_at) hint
 
+theorem integral_eq_sub_of_has_deriv_at_of_tendsto (hab : a < b) {fa fb}
+  (hderiv : ∀ x ∈ Ioo a b, has_deriv_at f (f' x) x) (hint : interval_integrable f' volume a b)
+  (ha : tendsto f (𝓝[Ioi a] a) (𝓝 fa)) (hb : tendsto f (𝓝[Iio b] b) (𝓝 fb)) :
+  ∫ y in a..b, f' y = fb - fa :=
+begin
+  set F : ℝ → E := update (update f a fa) b fb,
+  have Fderiv : ∀ x ∈ Ioo a b, has_deriv_at F (f' x) x,
+  { refine λ x hx, (hderiv x hx).congr_of_eventually_eq _,
+    filter_upwards [Ioo_mem_nhds hx.1 hx.2],
+    intros y hy, simp only [F],
+    rw [update_noteq hy.2.ne, update_noteq hy.1.ne'] },
+  have hcont : continuous_on F (Icc a b),
+  { rw [continuous_on_update_iff, continuous_on_update_iff, Icc_diff_right, Ico_diff_left],
+    refine ⟨⟨λ z hz, (hderiv z hz).continuous_at.continuous_within_at, _⟩, _⟩,
+    { exact λ _, ha.mono_left (nhds_within_mono _ Ioo_subset_Ioi_self) },
+    { rintro -,
+      refine (hb.congr' _).mono_left (nhds_within_mono _ Ico_subset_Iio_self),
+      filter_upwards [Ioo_mem_nhds_within_Iio (right_mem_Ioc.2 hab)],
+      exact λ z hz, (update_noteq hz.1.ne' _ _).symm } },
+  simpa [F, hab.ne, hab.ne'] using integral_eq_sub_of_has_deriv_at_of_le hab.le hcont Fderiv hint
+end
+
 /-- Fundamental theorem of calculus-2: If `f : ℝ → E` is differentiable at every `x` in `[a, b]` and
   its derivative is integrable on `[a, b]`, then `∫ y in a..b, deriv f y` equals `f b - f a`. -/
 theorem integral_deriv_eq_sub (hderiv : ∀ x ∈ interval a b, differentiable_at ℝ f x)

src/topology/continuous_on.lean

@@ -618,6 +618,17 @@ lemma continuous_within_at.diff_iff {f : α → β} {s t : set α} {x : α}
   continuous_within_at f (s \ {x}) x ↔ continuous_within_at f s x :=
 continuous_within_at_singleton.diff_iff
 
+lemma continuous_within_at_update_same [decidable_eq α] {f : α → β} {s : set α} {x : α} {y : β} :
+  continuous_within_at (function.update f x y) s x ↔ tendsto f (𝓝[s \ {x}] x) (𝓝 y) :=
+calc continuous_within_at (function.update f x y) s x
+    ↔ continuous_within_at (function.update f x y) (s \ {x}) x :
+  continuous_within_at_diff_self.symm
+... ↔ tendsto (function.update f x y) (𝓝[s \ {x}] x) (𝓝 y) :
+  by rw [continuous_within_at, function.update_same]
+... ↔ tendsto f (𝓝[s \ {x}] x) (𝓝 y) :
+  tendsto_congr' $ mem_of_superset self_mem_nhds_within $
+    λ z hz, by rw [mem_set_of_eq, function.update_noteq hz.2]
+
 theorem is_open_map.continuous_on_image_of_left_inv_on {f : α → β} {s : set α}
   (h : is_open_map (s.restrict f)) {finv : β → α} (hleft : left_inv_on finv f s) :
   continuous_on finv (f '' s) :=
@@ -755,10 +766,15 @@ lemma continuous_within_at.preimage_mem_nhds_within' {f : α → β} {x : α} {s
   f ⁻¹' t ∈ 𝓝[s] x :=
 h.tendsto_nhds_within (maps_to_image _ _) ht
 
+lemma filter.eventually_eq.congr_continuous_within_at {f g : α → β} {s : set α} {x : α}
+  (h : f =ᶠ[𝓝[s] x] g) (hx : f x = g x) :
+  continuous_within_at f s x ↔ continuous_within_at g s x :=
+by rw [continuous_within_at, hx, tendsto_congr' h, continuous_within_at]
+
 lemma continuous_within_at.congr_of_eventually_eq {f f₁ : α → β} {s : set α} {x : α}
   (h : continuous_within_at f s x) (h₁ : f₁ =ᶠ[𝓝[s] x] f) (hx : f₁ x = f x) :
   continuous_within_at f₁ s x :=
-by rwa [continuous_within_at, filter.tendsto, hx, filter.map_congr h₁]
+(h₁.congr_continuous_within_at hx).2 h
 
 lemma continuous_within_at.congr {f f₁ : α → β} {s : set α} {x : α}
   (h : continuous_within_at f s x) (h₁ : ∀y∈s, f₁ y = f y) (hx : f₁ x = f x) :

src/topology/separation.lean

@@ -222,6 +222,34 @@ is_closed_singleton.is_open_compl
 lemma is_open_ne [t1_space α] {x : α} : is_open {y | y ≠ x} :=
 is_open_compl_singleton
 
+lemma ne.nhds_within_compl_singleton [t1_space α] {x y : α} (h : x ≠ y) :
+  𝓝[{y}ᶜ] x = 𝓝 x :=
+is_open_ne.nhds_within_eq h
+
+lemma continuous_within_at_update_of_ne [t1_space α] [decidable_eq α] [topological_space β]
+  {f : α → β} {s : set α} {x y : α} {z : β} (hne : y ≠ x) :
+  continuous_within_at (function.update f x z) s y ↔ continuous_within_at f s y :=
+eventually_eq.congr_continuous_within_at
+  (mem_nhds_within_of_mem_nhds $ mem_of_superset (is_open_ne.mem_nhds hne) $
+    λ y' hy', function.update_noteq hy' _ _)
+  (function.update_noteq hne _ _)
+
+lemma continuous_on_update_iff [t1_space α] [decidable_eq α] [topological_space β]
+  {f : α → β} {s : set α} {x : α} {y : β} :
+  continuous_on (function.update f x y) s ↔
+    continuous_on f (s \ {x}) ∧ (x ∈ s → tendsto f (𝓝[s \ {x}] x) (𝓝 y)) :=
+begin
+  rw [continuous_on, ← and_forall_ne x, and_comm],
+  refine and_congr ⟨λ H z hz, _, λ H z hzx hzs, _⟩ (forall_congr $ λ hxs, _),
+  { specialize H z hz.2 hz.1,
+    rw continuous_within_at_update_of_ne hz.2 at H,
+    exact H.mono (diff_subset _ _) },
+  { rw continuous_within_at_update_of_ne hzx,
+    refine (H z ⟨hzs, hzx⟩).mono_of_mem (inter_mem_nhds_within _ _),
+    exact is_open_ne.mem_nhds hzx },
+  { exact continuous_within_at_update_same }
+end
+
 instance subtype.t1_space {α : Type u} [topological_space α] [t1_space α] {p : α → Prop} :
   t1_space (subtype p) :=
 ⟨λ ⟨x, hx⟩, is_closed_induced_iff.2 $ ⟨{x}, is_closed_singleton, set.ext $ λ y,