feat(measure_theory/integral/set_integral): remove or weaken some integrability assumptions (#18395)

When dealing with integrals on sets, we assume almost always that the set is measurable or null-measurable. However, there are situations where these assumptions can be removed, making the lemmas easier to apply, but at the cost of more involved proofs. We implement this in this PR. As an example, we prove `set_integral_eq_of_subset_of_forall_diff_eq_zero`: if `s` is contained in `t`, and `t` is null-measurable and a function vanishes on `t \ s`, then its integrals on `s` and `t` coincide (no measurability assumptions on `s` or `f`). The special case `t = univ` is especially useful.

Author: sgouezel

src/analysis/convolution.lean

@@ -211,7 +211,7 @@ lemma bdd_above.convolution_exists_at' {x₀ : G}
   (hf : integrable_on f s μ) (hmg : ae_strongly_measurable g $ map (λ t, x₀ - t) (μ.restrict s)) :
   convolution_exists_at f g x₀ L μ :=
 begin
-  rw [convolution_exists_at, ← integrable_on_iff_integrable_of_support_subset h2s hs],
+  rw [convolution_exists_at, ← integrable_on_iff_integrable_of_support_subset h2s],
   set s' := (λ t, - t + x₀) ⁻¹' s,
   have : ∀ᵐ (t : G) ∂(μ.restrict s),
     ‖L (f t) (g (x₀ - t))‖ ≤ s.indicator (λ t, ‖L‖ * ‖f t‖ * ⨆ i : s', ‖g i‖) t,

src/measure_theory/constructions/borel_space.lean

@@ -480,6 +480,11 @@ lemma measurable_set_lt [second_countable_topology α] {f g : δ → α} (hf : m
   (hg : measurable g) : measurable_set {a | f a < g a} :=
 hf.prod_mk hg measurable_set_lt'
 
+lemma null_measurable_set_lt [second_countable_topology α] {μ : measure δ} {f g : δ → α}
+  (hf : ae_measurable f μ) (hg : ae_measurable g μ) :
+  null_measurable_set {a | f a < g a} μ :=
+(hf.prod_mk hg).null_measurable measurable_set_lt'
+
 lemma set.ord_connected.measurable_set (h : ord_connected s) : measurable_set s :=
 begin
   let u := ⋃ (x ∈ s) (y ∈ s), Ioo x y,

src/measure_theory/function/conditional_expectation/basic.lean

@@ -856,7 +856,7 @@ lemma integral_norm_le_of_forall_fin_meas_integral_eq (hm : m ≤ m0) {f g : α
   (hs : measurable_set[m] s) (hμs : μ s ≠ ∞) :
   ∫ x in s, ‖g x‖ ∂μ ≤ ∫ x in s, ‖f x‖ ∂μ :=
 begin
-  rw [integral_norm_eq_pos_sub_neg (hg.mono hm) hgi, integral_norm_eq_pos_sub_neg hf hfi],
+  rw [integral_norm_eq_pos_sub_neg hgi, integral_norm_eq_pos_sub_neg hfi],
   have h_meas_nonneg_g : measurable_set[m] {x | 0 ≤ g x},
     from (@strongly_measurable_const _ _ m _ _).measurable_set_le hg,
   have h_meas_nonneg_f : measurable_set {x | 0 ≤ f x},

src/measure_theory/function/l1_space.lean

@@ -672,6 +672,22 @@ lemma mem_ℒp.integrable {q : ℝ≥0∞} (hq1 : 1 ≤ q) {f : α → β} [is_f
   (hfq : mem_ℒp f q μ) : integrable f μ :=
 mem_ℒp_one_iff_integrable.mp (hfq.mem_ℒp_of_exponent_le hq1)
 
+/-- A non-quantitative version of Markov inequality for integrable functions: the measure of points
+where `‖f x‖ ≥ ε` is finite for all positive `ε`. -/
+lemma integrable.measure_ge_lt_top {f : α → β} (hf : integrable f μ) {ε : ℝ} (hε : 0 < ε) :
+  μ {x | ε ≤ ‖f x‖} < ∞ :=
+begin
+  rw show {x | ε ≤ ‖f x‖} = {x | ennreal.of_real ε ≤ ‖f x‖₊},
+    by simp only [ennreal.of_real, real.to_nnreal_le_iff_le_coe, ennreal.coe_le_coe, coe_nnnorm],
+  refine (meas_ge_le_mul_pow_snorm μ one_ne_zero ennreal.one_ne_top hf.1 _).trans_lt _,
+  { simpa only [ne.def, ennreal.of_real_eq_zero, not_le] using hε },
+  apply ennreal.mul_lt_top,
+  { simpa only [ennreal.one_to_real, ennreal.rpow_one, ne.def, ennreal.inv_eq_top,
+      ennreal.of_real_eq_zero, not_le] using hε },
+  simpa only [ennreal.one_to_real, ennreal.rpow_one]
+    using (mem_ℒp_one_iff_integrable.2 hf).snorm_ne_top,
+end
+
 lemma lipschitz_with.integrable_comp_iff_of_antilipschitz {K K'} {f : α → β} {g : β → γ}
   (hg : lipschitz_with K g) (hg' : antilipschitz_with K' g) (g0 : g 0 = 0) :
   integrable (g ∘ f) μ ↔ integrable f μ :=

src/measure_theory/function/locally_integrable.lean

@@ -231,7 +231,7 @@ hf.integrable_on_Ioc
 /-- A continuous function with compact support is integrable on the whole space. -/
 lemma continuous.integrable_of_has_compact_support
   (hf : continuous f) (hcf : has_compact_support f) : integrable f μ :=
-(integrable_on_iff_integrable_of_support_subset (subset_tsupport f) measurable_set_closure).mp $
+(integrable_on_iff_integrable_of_support_subset (subset_tsupport f)).mp $
   hf.continuous_on.integrable_on_compact hcf
 
 end borel

src/measure_theory/function/strongly_measurable/basic.lean

@@ -113,7 +113,7 @@ open_locale measure_theory
 
 /-! ## Strongly measurable functions -/
 
-lemma strongly_measurable.ae_strongly_measurable {α β} {m0 : measurable_space α}
+protected lemma strongly_measurable.ae_strongly_measurable {α β} {m0 : measurable_space α}
   [topological_space β] {f : α → β} {μ : measure α} (hf : strongly_measurable f) :
   ae_strongly_measurable f μ :=
 ⟨f, hf, eventually_eq.refl _ _⟩
@@ -1425,6 +1425,41 @@ protected lemma indicator [has_zero β]
   ae_strongly_measurable (s.indicator f) μ :=
 (ae_strongly_measurable_indicator_iff hs).mpr hfm.restrict
 
+lemma null_measurable_set_eq_fun {E} [topological_space E] [metrizable_space E]
+  {f g : α → E} (hf : ae_strongly_measurable f μ) (hg : ae_strongly_measurable g μ) :
+  null_measurable_set {x | f x = g x} μ :=
+begin
+  apply (hf.strongly_measurable_mk.measurable_set_eq_fun hg.strongly_measurable_mk)
+    .null_measurable_set.congr,
+  filter_upwards [hf.ae_eq_mk, hg.ae_eq_mk] with x hfx hgx,
+  change (hf.mk f x = hg.mk g x) = (f x = g x),
+  simp only [hfx, hgx]
+end
+
+lemma null_measurable_set_lt
+  [linear_order β] [order_closed_topology β] [pseudo_metrizable_space β]
+  {f g : α → β} (hf : ae_strongly_measurable f μ)
+  (hg : ae_strongly_measurable g μ) :
+  null_measurable_set {a | f a < g a} μ :=
+begin
+  apply (hf.strongly_measurable_mk.measurable_set_lt hg.strongly_measurable_mk)
+    .null_measurable_set.congr,
+  filter_upwards [hf.ae_eq_mk, hg.ae_eq_mk] with x hfx hgx,
+  change (hf.mk f x < hg.mk g x) = (f x < g x),
+  simp only [hfx, hgx]
+end
+
+lemma null_measurable_set_le [preorder β] [order_closed_topology β] [pseudo_metrizable_space β]
+  {f g : α → β} (hf : ae_strongly_measurable f μ) (hg : ae_strongly_measurable g μ) :
+  null_measurable_set {a | f a ≤ g a} μ :=
+begin
+  apply (hf.strongly_measurable_mk.measurable_set_le hg.strongly_measurable_mk)
+    .null_measurable_set.congr,
+  filter_upwards [hf.ae_eq_mk, hg.ae_eq_mk] with x hfx hgx,
+  change (hf.mk f x ≤ hg.mk g x) = (f x ≤ g x),
+  simp only [hfx, hgx]
+end
+
 lemma _root_.ae_strongly_measurable_of_ae_strongly_measurable_trim {α} {m m0 : measurable_space α}
   {μ : measure α} (hm : m ≤ m0) {f : α → β} (hf : ae_strongly_measurable f (μ.trim hm)) :
   ae_strongly_measurable f μ :=

src/measure_theory/group/arithmetic.lean

@@ -336,6 +336,17 @@ begin
   simp_rw [set.mem_set_of_eq, pi.sub_apply, sub_eq_zero],
 end
 
+lemma null_measurable_set_eq_fun {E} [measurable_space E] [add_group E]
+  [measurable_singleton_class E] [has_measurable_sub₂ E] {f g : α → E}
+  (hf : ae_measurable f μ) (hg : ae_measurable g μ) :
+  null_measurable_set {x | f x = g x} μ :=
+begin
+  apply (measurable_set_eq_fun hf.measurable_mk hg.measurable_mk).null_measurable_set.congr,
+  filter_upwards [hf.ae_eq_mk, hg.ae_eq_mk] with x hfx hgx,
+  change (hf.mk f x = hg.mk g x) = (f x = g x),
+  simp only [hfx, hgx],
+end
+
 lemma measurable_set_eq_fun_of_countable {m : measurable_space α} {E} [measurable_space E]
   [measurable_singleton_class E] [countable E] {f g : α → E}
   (hf : measurable f) (hg : measurable g) :

src/measure_theory/integral/integrable_on.lean

@@ -231,12 +231,83 @@ begin
   simpa only [set.univ_inter, measurable_set.univ, measure.restrict_apply] using hμs,
 end
 
-lemma integrable_on_iff_integrable_of_support_subset {f : α → E} {s : set α}
-  (h1s : support f ⊆ s) (h2s : measurable_set s) :
+/-- If a function is integrable on a set `s` and nonzero there, then the measurable hull of `s` is
+well behaved: the restriction of the measure to `to_measurable μ s` coincides with its restriction
+to `s`. -/
+lemma integrable_on.restrict_to_measurable (hf : integrable_on f s μ) (h's : ∀ x ∈ s, f x ≠ 0) :
+  μ.restrict (to_measurable μ s) = μ.restrict s :=
+begin
+  rcases exists_seq_strict_anti_tendsto (0 : ℝ) with ⟨u, u_anti, u_pos, u_lim⟩,
+  let v := λ n, to_measurable (μ.restrict s) {x | u n ≤ ‖f x‖},
+  have A : ∀ n, μ (s ∩ v n) ≠ ∞,
+  { assume n,
+    rw [inter_comm, ← measure.restrict_apply (measurable_set_to_measurable _ _),
+      measure_to_measurable],
+    exact (hf.measure_ge_lt_top (u_pos n)).ne },
+  apply measure.restrict_to_measurable_of_cover _ A,
+  assume x hx,
+  have : 0 < ‖f x‖, by simp only [h's x hx, norm_pos_iff, ne.def, not_false_iff],
+  obtain ⟨n, hn⟩ : ∃ n, u n < ‖f x‖, from ((tendsto_order.1 u_lim).2 _ this).exists,
+  refine mem_Union.2 ⟨n, _⟩,
+  exact subset_to_measurable _ _ hn.le
+end
+
+/-- If a function is integrable on a set `s`, and vanishes on `t \ s`, then it is integrable on `t`
+if `t` is null-measurable. -/
+lemma integrable_on.of_ae_diff_eq_zero (hf : integrable_on f s μ)
+  (ht : null_measurable_set t μ) (h't : ∀ᵐ x ∂μ, x ∈ t \ s → f x = 0) :
+  integrable_on f t μ :=
+begin
+  let u := {x ∈ s | f x ≠ 0},
+  have hu : integrable_on f u μ := hf.mono_set (λ x hx, hx.1),
+  let v := to_measurable μ u,
+  have A : integrable_on f v μ,
+  { rw [integrable_on, hu.restrict_to_measurable],
+    { exact hu },
+    { assume x hx, exact hx.2 } },
+  have B : integrable_on f (t \ v) μ,
+  { apply integrable_on_zero.congr,
+    filter_upwards [ae_restrict_of_ae h't, ae_restrict_mem₀
+      (ht.diff (measurable_set_to_measurable μ u).null_measurable_set)] with x hxt hx,
+    by_cases h'x : x ∈ s,
+    { by_contra H,
+      exact hx.2 (subset_to_measurable μ u ⟨h'x, ne.symm H⟩) },
+    { exact (hxt ⟨hx.1, h'x⟩).symm, } },
+  apply (A.union B).mono_set _,
+  rw union_diff_self,
+  exact subset_union_right _ _
+end
+
+/-- If a function is integrable on a set `s`, and vanishes on `t \ s`, then it is integrable on `t`
+if `t` is measurable. -/
+lemma integrable_on.of_forall_diff_eq_zero (hf : integrable_on f s μ)
+  (ht : measurable_set t) (h't : ∀ x ∈ t \ s, f x = 0) :
+  integrable_on f t μ :=
+hf.of_ae_diff_eq_zero ht.null_measurable_set (eventually_of_forall h't)
+
+/-- If a function is integrable on a set `s` and vanishes almost everywhere on its complement,
+then it is integrable. -/
+lemma integrable_on.integrable_of_ae_not_mem_eq_zero (hf : integrable_on f s μ)
+  (h't : ∀ᵐ x ∂μ, x ∉ s → f x = 0) : integrable f μ :=
+begin
+  rw ← integrable_on_univ,
+  apply hf.of_ae_diff_eq_zero null_measurable_set_univ,
+  filter_upwards [h't] with x hx h'x using hx h'x.2,
+end
+
+/-- If a function is integrable on a set `s` and vanishes everywhere on its complement,
+then it is integrable. -/
+lemma integrable_on.integrable_of_forall_not_mem_eq_zero (hf : integrable_on f s μ)
+  (h't : ∀ x ∉ s, f x = 0) : integrable f μ :=
+hf.integrable_of_ae_not_mem_eq_zero (eventually_of_forall (λ x hx, h't x hx))
+
+lemma integrable_on_iff_integrable_of_support_subset (h1s : support f ⊆ s) :
   integrable_on f s μ ↔ integrable f μ :=
 begin
   refine ⟨λ h, _, λ h, h.integrable_on⟩,
-  rwa [← indicator_eq_self.2 h1s, integrable_indicator_iff h2s]
+  apply h.integrable_of_forall_not_mem_eq_zero (λ x hx, _),
+  contrapose! hx,
+  exact h1s (mem_support.2 hx),
 end
 
 lemma integrable_on_Lp_of_measure_ne_top {E} [normed_add_comm_group E]