feat(measure_theory): integral of a non-negative function is >0 iff μ…

…(support f) > 0 (#4410)

Also add a few supporting lemmas

src/algebra/order.lean

@@ -51,13 +51,19 @@ protected lemma ge [preorder α] {x y : α} (h : x = y) : y ≤ x := h.symm.le
 lemma trans_le [preorder α] {x y z : α} (h1 : x = y) (h2 : y ≤ z) : x ≤ z := h1.le.trans h2
 end eq
 
-namespace has_le
-namespace le
+namespace has_le.le
+
 @[nolint ge_or_gt] -- see Note [nolint_ge]
 protected lemma ge [has_le α] {x y : α} (h : x ≤ y) : y ≥ x := h
+
 lemma trans_eq [preorder α] {x y z : α} (h1 : x ≤ y) (h2 : y = z) : x ≤ z := h1.trans h2.le
-end le
-end has_le
+
+lemma lt_iff_ne [partial_order α] {x y : α} (h : x ≤ y) : x < y ↔ x ≠ y := ⟨λ h, h.ne, h.lt_of_ne⟩
+
+lemma le_iff_eq [partial_order α] {x y : α} (h : x ≤ y) : y ≤ x ↔ y = x :=
+⟨λ h', h'.antisymm h, eq.le⟩
+
+end has_le.le
 
 namespace has_lt
 namespace lt

src/data/indicator_function.lean

@@ -59,6 +59,21 @@ lemma eq_on_indicator : eq_on (indicator s f) f s := λ x hx, indicator_of_mem h
 lemma support_indicator : function.support (s.indicator f) ⊆ s :=
 λ x hx, hx.imp_symm (λ h, indicator_of_not_mem h f)
 
+lemma indicator_of_support_subset (h : support f ⊆ s) : s.indicator f = f :=
+begin
+  ext x,
+  by_cases hx : f x = 0,
+  { rw hx,
+    by_contradiction H,
+    have := mem_of_indicator_ne_zero H,
+    rw [indicator_of_mem this f, hx] at H,
+    exact H rfl },
+  { exact indicator_of_mem (h hx) f }
+end
+
+@[simp] lemma indicator_support : (support f).indicator f = f :=
+indicator_of_support_subset $ subset.refl _
+
 @[simp] lemma indicator_range_comp {ι : Sort*} (f : ι → α) (g : α → β) :
   indicator (range f) g ∘ f = g ∘ f :=
 piecewise_range_comp _ _ _

src/data/support.lean

@@ -6,6 +6,7 @@ Authors: Yury Kudryashov
 import order.conditionally_complete_lattice
 import algebra.big_operators.basic
 import algebra.group.prod
+import algebra.group.pi
 
 /-!
 # Support of a function
@@ -40,6 +41,10 @@ lemma support_subset_iff' [has_zero A] {f : α → A} {s : set α} :
   support f ⊆ s ↔ ∀ x ∉ s, f x = 0 :=
 forall_congr $ λ x, by classical; exact not_imp_comm
 
+@[simp] lemma support_eq_empty_iff [has_zero A] {f : α → A} :
+  support f = ∅ ↔ f = 0 :=
+by { simp_rw [← subset_empty_iff, support_subset_iff', funext_iff], simp }
+
 lemma support_binop_subset [has_zero A] (op : A → A → A) (op0 : op 0 0 = 0) (f g : α → A) :
   support (λ x, op (f x) (g x)) ⊆ support f ∪ support g :=
 λ x hx, classical.by_cases

src/measure_theory/bochner_integration.lean

@@ -1198,6 +1198,27 @@ end
 lemma integral_nonpos {f : α → ℝ} (hf : f ≤ 0) : ∫ a, f a ∂μ ≤ 0 :=
 integral_nonpos_of_ae $ eventually_of_forall hf
 
+lemma integral_eq_zero_iff_of_nonneg_ae {f : α → ℝ} (hf : 0 ≤ᵐ[μ] f) (hfi : integrable f μ) :
+  ∫ x, f x ∂μ = 0 ↔ f =ᵐ[μ] 0 :=
+by simp_rw [integral_eq_lintegral_of_nonneg_ae hf hfi.1, ennreal.to_real_eq_zero_iff,
+  lintegral_eq_zero_iff (ennreal.measurable_of_real.comp hfi.1), ← ennreal.not_lt_top,
+  ← has_finite_integral_iff_of_real hf, hfi.2, not_true, or_false, ← hf.le_iff_eq,
+  filter.eventually_eq, filter.eventually_le, (∘), pi.zero_apply, ennreal.of_real_eq_zero]
+
+lemma integral_eq_zero_iff_of_nonneg {f : α → ℝ} (hf : 0 ≤ f) (hfi : integrable f μ) :
+  ∫ x, f x ∂μ = 0 ↔ f =ᵐ[μ] 0 :=
+integral_eq_zero_iff_of_nonneg_ae (eventually_of_forall hf) hfi
+
+lemma integral_pos_iff_support_of_nonneg_ae {f : α → ℝ} (hf : 0 ≤ᵐ[μ] f) (hfi : integrable f μ) :
+  (0 < ∫ x, f x ∂μ) ↔ 0 < μ (function.support f) :=
+by simp_rw [(integral_nonneg_of_ae hf).lt_iff_ne, zero_lt_iff_ne_zero, ne.def, @eq_comm ℝ 0,
+  integral_eq_zero_iff_of_nonneg_ae hf hfi, filter.eventually_eq, ae_iff, pi.zero_apply,
+  function.support]
+
+lemma integral_pos_iff_support_of_nonneg {f : α → ℝ} (hf : 0 ≤ f) (hfi : integrable f μ) :
+  (0 < ∫ x, f x ∂μ) ↔ 0 < μ (function.support f) :=
+integral_pos_iff_support_of_nonneg_ae (eventually_of_forall hf) hfi
+
 section normed_group
 variables {H : Type*} [normed_group H] [second_countable_topology H] [measurable_space H]
           [borel_space H]

src/measure_theory/integration.lean

@@ -1178,7 +1178,7 @@ lemma meas_ge_le_lintegral_div {f : α → ennreal} (hf : measurable f) {ε : en
 (ennreal.le_div_iff_mul_le (or.inl hε) (or.inl hε')).2 $
 by { rw [mul_comm], exact mul_meas_ge_le_lintegral hf ε }
 
-lemma lintegral_eq_zero_iff {f : α → ennreal} (hf : measurable f) :
+@[simp] lemma lintegral_eq_zero_iff {f : α → ennreal} (hf : measurable f) :
   ∫⁻ a, f a ∂μ = 0 ↔ (f =ᵐ[μ] 0) :=
 begin
   refine iff.intro (assume h, _) (assume h, _),
@@ -1199,6 +1199,10 @@ begin
       ... = 0 : lintegral_zero }
 end
 
+lemma lintegral_pos_iff_support {f : α → ennreal} (hf : measurable f) :
+  0 < ∫⁻ a, f a ∂μ ↔ 0 < μ (function.support f) :=
+by simp [zero_lt_iff_ne_zero, hf, filter.eventually_eq, ae_iff, function.support]
+
 /-- Weaker version of the monotone convergence theorem-/
 lemma lintegral_supr_ae {f : ℕ → α → ennreal} (hf : ∀n, measurable (f n))
   (h_mono : ∀n, ∀ᵐ a ∂μ, f n a ≤ f n.succ a) :

src/measure_theory/interval_integral.lean

@@ -143,6 +143,11 @@ intervals is always empty, so this property is equivalent to `f` being integrabl
 def interval_integrable (f : α → E) (μ : measure α) (a b : α) :=
 integrable_on f (Ioc a b) μ ∧ integrable_on f (Ioc b a) μ
 
+lemma measure_theory.integrable.interval_integrable {f : α → E} {μ : measure α}
+  (hf : integrable f μ) {a b : α} :
+  interval_integrable f μ a b :=
+⟨hf.integrable_on, hf.integrable_on⟩
+
 namespace interval_integrable
 
 section
@@ -244,6 +249,9 @@ section
 
 variables {a b c d : α} {f g : α → E} {μ : measure α}
 
+@[simp] lemma integral_zero : ∫ x in a..b, (0 : E) ∂μ = 0 :=
+by simp [interval_integral]
+
 lemma integral_of_le (h : a ≤ b) : ∫ x in a..b, f x ∂μ = ∫ x in Ioc a b, f x ∂μ :=
 by simp [interval_integral, h]
 
@@ -261,6 +269,10 @@ lemma integral_cases (f : α → E) (a b) :
     -∫ x in Ioc (min a b) (max a b), f x ∂μ} : set E) :=
 (le_total a b).imp (λ h, by simp [h, integral_of_le]) (λ h, by simp [h, integral_of_ge])
 
+lemma integral_non_measurable {f : α → E} {a b} (hf : ¬measurable f) :
+  ∫ x in a..b, f x ∂μ = 0 :=
+by rw [interval_integral, integral_non_measurable hf, integral_non_measurable hf, sub_zero]
+
 lemma norm_integral_eq_norm_integral_Ioc :
   ∥∫ x in a..b, f x ∂μ∥ = ∥∫ x in Ioc (min a b) (max a b), f x ∂μ∥ :=
 (integral_cases f a b).elim (congr_arg _) (λ h, (congr_arg _ h).trans (norm_neg _))
@@ -348,7 +360,8 @@ end
 ### Integral is an additive function of the interval
 
 In this section we prove that `∫ x in a..b, f x ∂μ + ∫ x in b..c, f x ∂μ = ∫ x in a..c, f x ∂μ`
-as well as a few other identities trivially equivalent to this one.
+as well as a few other identities trivially equivalent to this one. We also prove that
+`∫ x in a..b, f x ∂μ = ∫ x, f x ∂μ` provided that `support f ⊆ Ioc a b`.
 -/
 
 variables [topological_space α] [opens_measurable_space α]
@@ -419,10 +432,58 @@ 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) :
+  ∫ x in a..b, f x ∂μ = ∫ x, f x ∂μ :=
+begin
+  by_cases hfm : measurable f,
+  { cases le_total a b with hab hab,
+    { rw [integral_of_le hab, ← integral_indicator hfm is_measurable_Ioc,
+        indicator_of_support_subset h] },
+    { rw [Ioc_eq_empty hab, subset_empty_iff, function.support_eq_empty_iff] at h,
+      simp [h] } },
+  { rw [integral_non_measurable hfm, measure_theory.integral_non_measurable hfm] },
+end
+
 end order_closed_topology
 
 end
 
+lemma integral_eq_zero_iff_of_le_of_nonneg_ae {f : ℝ → ℝ} {a b : ℝ} (hab : a ≤ b)
+  (hf : 0 ≤ᵐ[volume.restrict (Ioc a b)] f) (hfi : interval_integrable f volume a b) :
+  ∫ x in a..b, f x = 0 ↔ f =ᵐ[volume.restrict (Ioc a b)] 0 :=
+by rw [integral_of_le hab, integral_eq_zero_iff_of_nonneg_ae hf hfi.1]
+
+lemma integral_eq_zero_iff_of_nonneg_ae {f : ℝ → ℝ} {a b : ℝ}
+  (hf : 0 ≤ᵐ[volume.restrict (Ioc a b ∪ Ioc b a)] f) (hfi : interval_integrable f volume a b) :
+  ∫ x in a..b, f x = 0 ↔ f =ᵐ[volume.restrict (Ioc a b ∪ Ioc b a)] 0 :=
+begin
+  cases le_total a b with hab hab;
+    simp only [Ioc_eq_empty hab, empty_union, union_empty] at *,
+  { exact integral_eq_zero_iff_of_le_of_nonneg_ae hab hf hfi },
+  { rw [integral_symm, neg_eq_zero],
+    exact integral_eq_zero_iff_of_le_of_nonneg_ae hab hf hfi.symm }
+end
+
+lemma integral_pos_iff_support_of_nonneg_ae' {f : ℝ → ℝ} {a b : ℝ}
+  (hf : 0 ≤ᵐ[volume.restrict (Ioc a b ∪ Ioc b a)] f) (hfi : interval_integrable f volume a b) :
+  0 < ∫ x in a..b, f x ↔ a < b ∧ 0 < volume (function.support f ∩ Ioc a b) :=
+begin
+  cases le_total a b with hab hab,
+  { simp only [integral_of_le hab, Ioc_eq_empty hab, union_empty] at hf ⊢,
+    symmetry,
+    rw [set_integral_pos_iff_support_of_nonneg_ae hf hfi.1, and_iff_right_iff_imp],
+    contrapose!,
+    intro h,
+    simp [Ioc_eq_empty h] },
+  { rw [Ioc_eq_empty hab, empty_union] at hf,
+    simp [integral_of_ge hab, Ioc_eq_empty hab, integral_nonneg_of_ae hf] }
+end
+
+lemma integral_pos_iff_support_of_nonneg_ae {f : ℝ → ℝ} {a b : ℝ}
+  (hf : 0 ≤ᵐ[volume] f) (hfi : interval_integrable f volume a b) :
+  0 < ∫ x in a..b, f x ↔ a < b ∧ 0 < volume (function.support f ∩ Ioc a b) :=
+integral_pos_iff_support_of_nonneg_ae' (ae_mono measure.restrict_le_self hf) hfi
+
 /-!
 ### Fundamental theorem of calculus, part 1, for any measure
 

src/measure_theory/lebesgue_measure.lean

@@ -298,6 +298,17 @@ eq.symm $ real.measure_ext_Ioo_rat $ λ p q,
   by simp [measure.map_apply measurable_neg is_measurable_Ioo]
 
 end real
+
+open_locale topological_space
+
+lemma filter.eventually.volume_pos_of_nhds_real {p : ℝ → Prop} {a : ℝ} (h : ∀ᶠ x in 𝓝 a, p x) :
+  (0 : ennreal) < volume {x | p x} :=
+begin
+  rcases h.exists_Ioo_subset with ⟨l, u, hx, hs⟩,
+  refine lt_of_lt_of_le _ (measure_mono hs),
+  simpa [-mem_Ioo] using hx.1.trans hx.2
+end
+
 /-
 section vitali
 

src/measure_theory/set_integral.lean

@@ -391,6 +391,17 @@ lemma norm_set_integral_le_of_norm_le_const' {C : ℝ} (hs : μ s < ⊤) (hsm :
   ∥∫ x in s, f x ∂μ∥ ≤ C * (μ s).to_real :=
 norm_set_integral_le_of_norm_le_const_ae'' hs hsm $ eventually_of_forall hC
 
+lemma set_integral_eq_zero_iff_of_nonneg_ae {f : α → ℝ} (hf : 0 ≤ᵐ[μ.restrict s] f)
+  (hfi : integrable_on f s μ) :
+  ∫ x in s, f x ∂μ = 0 ↔ f =ᵐ[μ.restrict s] 0 :=
+integral_eq_zero_iff_of_nonneg_ae hf hfi
+
+lemma set_integral_pos_iff_support_of_nonneg_ae {f : α → ℝ} (hf : 0 ≤ᵐ[μ.restrict s] f)
+  (hfi : integrable_on f s μ) :
+  0 < ∫ x in s, f x ∂μ ↔ 0 < μ (support f ∩ s) :=
+by { rw [integral_pos_iff_support_of_nonneg_ae hf hfi, measure.restrict_apply],
+  exact hfi.1 (is_measurable_singleton 0).compl }
+
 end normed_group
 
 end measure_theory
@@ -452,6 +463,18 @@ lemma continuous.integrable_on_compact
   integrable_on f s μ :=
 hf.continuous_on.integrable_on_compact hs hf.measurable
 
+/-- A continuous function with compact closure of the support is integrable on the whole space. -/
+lemma continuous.integrable_of_compact_closure_support
+  [topological_space α] [opens_measurable_space α] [t2_space α] [borel_space E]
+  {μ : measure α} [locally_finite_measure μ] {f : α → E} (hf : continuous f)
+  (hfc : is_compact (closure $ support f)) :
+  integrable f μ :=
+begin
+  rw [← indicator_of_support_subset (@subset_closure _ _ (support f)),
+    integrable_indicator_iff hf.measurable is_closed_closure.is_measurable],
+  exact hf.integrable_on_compact hfc
+end
+
 /-- Fundamental theorem of calculus for set integrals, `nhds` version: if `μ` is a locally finite
 measure that and `f` is a measurable function that is continuous at a point `a`,
 then `∫ x in s, f x ∂μ = μ s • f a + o(μ s)` as `s` tends to `(𝓝 a).lift' powerset`.

src/order/filter/basic.lean

@@ -1293,6 +1293,10 @@ lemma eventually_le_antisymm_iff [partial_order β] {l : filter α} {f g : α 
   f =ᶠ[l] g ↔ f ≤ᶠ[l] g ∧ g ≤ᶠ[l] f :=
 by simp only [eventually_eq, eventually_le, le_antisymm_iff, eventually_and]
 
+lemma eventually_le.le_iff_eq [partial_order β] {l : filter α} {f g : α → β} (h : f ≤ᶠ[l] g) :
+  g ≤ᶠ[l] f ↔ g =ᶠ[l] f :=
+⟨λ h', h'.antisymm h, eventually_eq.le⟩
+
 lemma join_le {f : filter (filter α)} {l : filter α} (h : ∀ᶠ m in f, m ≤ l) : join f ≤ l :=
 λ s hs, h.mono $ λ m hm, hm hs
 

src/topology/algebra/ordered.lean

@@ -938,11 +938,17 @@ begin
     apply mem_sets_of_superset (mem_nhds_sets is_open_Ioo ha) h }
 end
 
-/-- A set is a neighborhood of `a` if and only if it contains an interval `(l, u)` containing `a`. -/
+/-- A set is a neighborhood of `a` if and only if it contains an interval `(l, u)` containing `a`.
+-/
 lemma mem_nhds_iff_exists_Ioo_subset [no_top_order α] [no_bot_order α] {a : α} {s : set α} :
   s ∈ 𝓝 a ↔ ∃l u, a ∈ Ioo l u ∧ Ioo l u ⊆ s :=
 let ⟨l', hl'⟩ := no_bot a in let ⟨u', hu'⟩ := no_top a in mem_nhds_iff_exists_Ioo_subset' hl' hu'
 
+lemma filter.eventually.exists_Ioo_subset [no_top_order α] [no_bot_order α] {a : α} {p : α → Prop}
+  (hp : ∀ᶠ x in 𝓝 a, p x) :
+  ∃ l u, a ∈ Ioo l u ∧ Ioo l u ⊆ {x | p x} :=
+mem_nhds_iff_exists_Ioo_subset.1 hp
+
 lemma Iio_mem_nhds {a b : α} (h : a < b) : Iio b ∈ 𝓝 a :=
 mem_nhds_sets is_open_Iio h
 

src/topology/basic.lean

@@ -502,6 +502,10 @@ lemma mem_nhds_sets {a : α} {s : set α} (hs : is_open s) (ha : a ∈ s) :
   s ∈ 𝓝 a :=
 mem_nhds_sets_iff.2 ⟨s, subset.refl _, hs, ha⟩
 
+lemma is_open.eventually_mem {a : α} {s : set α} (hs : is_open s) (ha : a ∈ s) :
+  ∀ᶠ x in 𝓝 a, x ∈ s :=
+mem_nhds_sets hs ha
+
 /-- The open neighborhoods of `a` are a basis for the neighborhood filter. See `nhds_basis_opens`
 for a variant using open sets around `a` instead. -/
 lemma nhds_basis_opens' (a : α) : (𝓝 a).has_basis (λ s : set α, s ∈ 𝓝 a ∧ is_open s) (λ x, x) :=