[Merged by Bors] - feat(measure_theory/interval_integral): more versions of FTC-1

src/data/set/intervals/disjoint.lean

@@ -20,6 +20,20 @@ variables {α : Type u}
 
 namespace set
 
+section preorder
+variables [preorder α] {a b c : α}
+
+@[simp] lemma Iic_disjoint_Ioi (h : a ≤ b) : disjoint (Iic a) (Ioi b) :=
+λ x ⟨ha, hb⟩, not_le_of_lt (h.trans_lt hb) ha
+
+lemma Iic_disjoint_Ioc (h : a ≤ b) : disjoint (Iic a) (Ioc b c) :=
+(Iic_disjoint_Ioi h).mono (le_refl _) (λ _, and.left)
+
+lemma Ioc_disjoint_Ioc_same {a b c : α} : disjoint (Ioc a b) (Ioc b c) :=
+(Iic_disjoint_Ioc (le_refl b)).mono (λ _, and.right) (le_refl _)
+
+end preorder
+
 section decidable_linear_order
 variables [decidable_linear_order α] {a₁ a₂ b₁ b₂ : α}
 
@@ -33,9 +47,6 @@ lemma Ico_disjoint_Ico_same {a b c : α} : disjoint (Ico a b) (Ico b c) :=
 lemma Ioc_disjoint_Ioc : disjoint (Ioc a₁ a₂) (Ioc b₁ b₂) ↔ min a₂ b₂ ≤ max a₁ b₁ :=
 by simpa only [dual_Ico] using @Ico_disjoint_Ico (order_dual α) _ a₂ a₁ b₂ b₁
 
-lemma Ioc_disjoint_Ioc_same {a b c : α} : disjoint (Ioc a b) (Ioc b c) :=
-λ x hx, not_le.2 hx.2.1 hx.1.2
-
 /-- If two half-open intervals are disjoint and the endpoint of one lies in the other,
   then it must be equal to the endpoint of the other. -/
 lemma eq_of_Ico_disjoint {x₁ x₂ y₁ y₂ : α}

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

src/measure_theory/l1_space.lean

@@ -121,7 +121,7 @@ begin
 end
 
 lemma integrable_const [finite_measure μ] (c : β) : integrable (λ x : α, c) μ :=
-integrable_const_iff.2 (or.inr meas_univ_lt_top)
+integrable_const_iff.2 (or.inr $ measure_lt_top _ _)
 
 lemma integrable_of_bounded [finite_measure μ] {f : α → β} {C : ℝ} (hC : ∀ᵐ a ∂μ, ∥f a∥ ≤ C) :
   integrable f μ :=

src/measure_theory/measure_space.lean

@@ -1034,25 +1034,31 @@ lemma restrict_congr {s t : set α} (H : s =ᵐ[μ] t) : μ.restrict s = μ.rest
 le_antisymm (restrict_mono_ae H.le) (restrict_mono_ae H.symm.le)
 
 /-- A measure `μ` is called a probability measure if `μ univ = 1`. -/
-class probability_measure (μ : measure α) : Prop := (meas_univ : μ univ = 1)
+class probability_measure (μ : measure α) : Prop := (measure_univ : μ univ = 1)
 
 /-- A measure `μ` is called finite if `μ univ < ⊤`. -/
-class finite_measure (μ : measure α) : Prop := (meas_univ_lt_top : μ univ < ⊤)
+class finite_measure (μ : measure α) : Prop := (measure_univ_lt_top : μ univ < ⊤)
 
-export finite_measure (meas_univ_lt_top) probability_measure (meas_univ)
+export probability_measure (measure_univ)
+
+lemma measure_lt_top (μ : measure α) [finite_measure μ] (s : set α) : μ s < ⊤ :=
+(measure_mono (subset_univ s)).trans_lt finite_measure.measure_univ_lt_top
+
+lemma measure_ne_top (μ : measure α) [finite_measure μ] (s : set α) : μ s ≠ ⊤ :=
+ne_of_lt (measure_lt_top μ s)
 
 @[priority 100]
 instance probability_measure.to_finite_measure (μ : measure α) [probability_measure μ] :
   finite_measure μ :=
-⟨by simp only [meas_univ, ennreal.one_lt_top]⟩
+⟨by simp only [measure_univ, ennreal.one_lt_top]⟩
 
 /-- A measure is called finite at filter `f` if it is finite at some set `s ∈ f`.
 Equivalently, it is eventually finite at `s` in `f.lift' powerset`. -/
 def measure.finite_at_filter (μ : measure α) (f : filter α) : Prop := ∃ s ∈ f, μ s < ⊤
 
 lemma finite_at_filter_of_finite (μ : measure α) [finite_measure μ] (f : filter α) :
   μ.finite_at_filter f :=
-⟨univ, univ_mem_sets, meas_univ_lt_top⟩
+⟨univ, univ_mem_sets, measure_lt_top μ univ⟩
 
 /-- A measure is called locally finite if it is finite in some neighborhood of each point. -/
 class locally_finite_measure [topological_space α] (μ : measure α) : Prop :=

src/measure_theory/set_integral.lean

@@ -241,10 +241,10 @@ begin
 end
 
 lemma measure.finite_at_filter.integrable_at_filter_of_tendsto_ae
-  {l : filter α} [is_measurably_generated l] (hμ : μ.finite_at_filter (l ⊓ μ.ae)) {b}
+  {l : filter α} [is_measurably_generated l] (hμ : μ.finite_at_filter l) {b}
   (hf : tendsto f (l ⊓ μ.ae) (𝓝 b)) :
   integrable_at_filter f l μ :=
-(hμ.integrable_at_filter hf.norm.is_bounded_under_le).of_inf_ae
+(hμ.inf_of_left.integrable_at_filter hf.norm.is_bounded_under_le).of_inf_ae
 
 alias measure.finite_at_filter.integrable_at_filter_of_tendsto_ae ←
   filter.tendsto.integrable_at_filter_ae
@@ -344,7 +344,7 @@ begin
   intros ε ε₀,
   have : ∀ᶠ s in l.lift' powerset, ∀ᶠ x in μ.ae, x ∈ s → f x ∈ closed_ball b ε :=
     eventually_lift'_powerset_eventually.2 (h.eventually $ closed_ball_mem_nhds _ ε₀),
-  refine hμ.eventually.mp ((h.integrable_at_filter_ae hμ.inf_of_left).eventually.mp (this.mono _)),
+  refine hμ.eventually.mp ((h.integrable_at_filter_ae hμ).eventually.mp (this.mono _)),
   simp only [mem_closed_ball, dist_eq_norm],
   intros s h_norm h_integrable hμs,
   rw [← set_integral_const, ← integral_sub hfm h_integrable measurable_const

src/topology/continuous_on.lean

@@ -103,9 +103,12 @@ inter_mem_sets (mem_inf_sets_of_right (mem_principal_self s)) (mem_inf_sets_of_l
 theorem nhds_within_mono (a : α) {s t : set α} (h : s ⊆ t) : 𝓝[s] a ≤ 𝓝[t] a :=
 inf_le_inf_left _ (principal_mono.mpr h)
 
+lemma pure_le_nhds_within {a : α} {s : set α} (ha : a ∈ s) : pure a ≤ 𝓝[s] a :=
+le_inf (pure_le_nhds a) (le_principal_iff.2 ha)
+
 lemma mem_of_mem_nhds_within {a : α} {s t : set α} (ha : a ∈ s) (ht : t ∈ 𝓝[s] a) :
   a ∈ t :=
-let ⟨u, hu, H⟩ := mem_nhds_within.1 ht in H.2 ⟨H.1, ha⟩
+pure_le_nhds_within ha ht
 
 lemma filter.eventually.self_of_nhds_within {p : α → Prop} {s : set α} {x : α}
   (h : ∀ᶠ y in 𝓝[s] x, p y) (hx : x ∈ s) : p x :=