feat(measure_theory/conditional_expectation): the integral of the nor…

…m of the conditional expectation is lower (#8318)

Let `m` be a sub-σ-algebra of `m0`, `f` a `m0`-measurable function and `g` a `m`-measurable function, such that their integrals coincide on `m`-measurable sets with finite measure. Then `∫ x in s, ∥g x∥ ∂μ ≤ ∫ x in s, ∥f x∥ ∂μ` on all `m`-measurable sets with finite measure.

This PR also defines a notation `measurable[m] f`, to mean that `f : α → β` is measurable with respect to the `measurable_space` `m` on `α`.



Co-authored-by: RemyDegenne <remydegenne@gmail.com>

src/algebra/indicator_function.lean

@@ -470,6 +470,22 @@ mul_indicator_le' hfg $ λ _ _, one_le _
 
 end canonically_ordered_monoid
 
+lemma indicator_le_indicator_nonneg {β} [linear_order β] [has_zero β] (s : set α) (f : α → β) :
+  s.indicator f ≤ {x | 0 ≤ f x}.indicator f :=
+begin
+  intro x,
+  simp_rw indicator_apply,
+  split_ifs,
+  { exact le_rfl, },
+  { exact (not_le.mp h_1).le, },
+  { exact h_1, },
+  { exact le_rfl, },
+end
+
+lemma indicator_nonpos_le_indicator {β} [linear_order β] [has_zero β] (s : set α) (f : α → β) :
+  {x | f x ≤ 0}.indicator f ≤ s.indicator f :=
+@indicator_le_indicator_nonneg α (order_dual β) _ _ s f
+
 end set
 
 @[to_additive] lemma monoid_hom.map_mul_indicator {M N : Type*} [monoid M] [monoid N] (f : M →* N)

src/measure_theory/function/conditional_expectation.lean

@@ -437,6 +437,65 @@ end
 
 end uniqueness_of_conditional_expectation
 
+
+section integral_norm_le
+
+variables {m m0 : measurable_space α} {μ : measure α} {s : set α}
+
+/-- Let `m` be a sub-σ-algebra of `m0`, `f` a `m0`-measurable function and `g` a `m`-measurable
+function, such that their integrals coincide on `m`-measurable sets with finite measure.
+Then `∫ x in s, ∥g x∥ ∂μ ≤ ∫ x in s, ∥f x∥ ∂μ` on all `m`-measurable sets with finite measure. -/
+lemma integral_norm_le_of_forall_fin_meas_integral_eq (hm : m ≤ m0) {f g : α → ℝ}
+  (hf : measurable f) (hfi : integrable_on f s μ) (hg : measurable[m] g) (hgi : integrable_on g s μ)
+  (hgf : ∀ t, measurable_set[m] t → μ t < ∞ → ∫ x in t, g x ∂μ = ∫ x in t, f x ∂μ)
+  (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 le_rfl) hgi, integral_norm_eq_pos_sub_neg hf hfi],
+  have h_meas_nonneg_g : measurable_set[m] {x | 0 ≤ g x},
+    from @measurable_set_le _ α _ _ _ m _ _ _ _ g (@measurable_const _ α _ m _) hg,
+  have h_meas_nonneg_f : measurable_set {x | 0 ≤ f x},
+    from measurable_set_le measurable_const hf,
+  have h_meas_nonpos_g : measurable_set[m] {x | g x ≤ 0},
+    from @measurable_set_le _ α _ _ _ m _ _ _ g _ hg (@measurable_const _ α _ m _),
+  have h_meas_nonpos_f : measurable_set {x | f x ≤ 0},
+    from measurable_set_le hf measurable_const,
+  refine sub_le_sub _ _,
+  { rw [measure.restrict_restrict (hm _ h_meas_nonneg_g),
+      measure.restrict_restrict h_meas_nonneg_f,
+      hgf _ (@measurable_set.inter α m _ _ h_meas_nonneg_g hs)
+        ((measure_mono (set.inter_subset_right _ _)).trans_lt (lt_top_iff_ne_top.mpr hμs)),
+      ← measure.restrict_restrict (hm _ h_meas_nonneg_g),
+      ← measure.restrict_restrict h_meas_nonneg_f],
+    exact set_integral_le_nonneg (hm _ h_meas_nonneg_g) hf hfi, },
+  { rw [measure.restrict_restrict (hm _ h_meas_nonpos_g),
+      measure.restrict_restrict h_meas_nonpos_f,
+      hgf _ (@measurable_set.inter α m _ _ h_meas_nonpos_g hs)
+        ((measure_mono (set.inter_subset_right _ _)).trans_lt (lt_top_iff_ne_top.mpr hμs)),
+      ← measure.restrict_restrict (hm _ h_meas_nonpos_g),
+      ← measure.restrict_restrict h_meas_nonpos_f],
+    exact set_integral_nonpos_le (hm _ h_meas_nonpos_g) hf hfi, },
+end
+
+/-- Let `m` be a sub-σ-algebra of `m0`, `f` a `m0`-measurable function and `g` a `m`-measurable
+function, such that their integrals coincide on `m`-measurable sets with finite measure.
+Then `∫⁻ x in s, ∥g x∥₊ ∂μ ≤ ∫⁻ x in s, ∥f x∥₊ ∂μ` on all `m`-measurable sets with finite
+measure. -/
+lemma lintegral_nnnorm_le_of_forall_fin_meas_integral_eq (hm : m ≤ m0) {f g : α → ℝ}
+  (hf : measurable f) (hfi : integrable_on f s μ) (hg : measurable[m] g) (hgi : integrable_on g s μ)
+  (hgf : ∀ t, measurable_set[m] t → μ t < ∞ → ∫ x in t, g x ∂μ = ∫ x in t, f x ∂μ)
+  (hs : measurable_set[m] s) (hμs : μ s ≠ ∞) :
+  ∫⁻ x in s, ∥g x∥₊ ∂μ ≤ ∫⁻ x in s, ∥f x∥₊ ∂μ :=
+begin
+  rw [← of_real_integral_norm_eq_lintegral_nnnorm hfi,
+    ← of_real_integral_norm_eq_lintegral_nnnorm hgi, ennreal.of_real_le_of_real_iff],
+  { exact integral_norm_le_of_forall_fin_meas_integral_eq hm hf hfi hg hgi hgf hs hμs, },
+  { exact integral_nonneg (λ x, norm_nonneg _), },
+end
+
+end integral_norm_le
+
+
 /-! ## Conditional expectation in L2
 
 We define a conditional expectation in `L2`: it is the orthogonal projection on the subspace

src/measure_theory/integral/bochner.lean

@@ -965,6 +965,15 @@ begin
     rw [this, hfi], refl }
 end
 
+lemma of_real_integral_norm_eq_lintegral_nnnorm {G} [normed_group G] [measurable_space G]
+  [opens_measurable_space G] {f : α → G} (hf : integrable f μ) :
+  ennreal.of_real ∫ x, ∥f x∥ ∂μ = ∫⁻ x, ∥f x∥₊ ∂μ :=
+begin
+  rw integral_eq_lintegral_of_nonneg_ae _ hf.1.norm,
+  { simp_rw [of_real_norm_eq_coe_nnnorm, ennreal.of_real_to_real (lt_top_iff_ne_top.mp hf.2)], },
+  { refine ae_of_all _ _, simp, },
+end
+
 lemma integral_eq_integral_pos_part_sub_integral_neg_part {f : α → ℝ} (hf : integrable f μ) :
   ∫ a, f a ∂μ = (∫ a, real.to_nnreal (f a) ∂μ) - (∫ a, real.to_nnreal (-f a) ∂μ) :=
 begin

src/measure_theory/integral/lebesgue.lean

@@ -1069,6 +1069,11 @@ lemma set_lintegral_congr {f : α → ℝ≥0∞} {s t : set α} (h : s =ᵐ[μ]
   ∫⁻ x in s, f x ∂μ = ∫⁻ x in t, f x ∂μ :=
 by rw [restrict_congr_set h]
 
+lemma set_lintegral_congr_fun {f g : α → ℝ≥0∞} {s : set α} (hs : measurable_set s)
+  (hfg : ∀ᵐ x ∂μ, x ∈ s → f x = g x) :
+  ∫⁻ x in s, f x ∂μ = ∫⁻ x in s, g x ∂μ :=
+by { rw lintegral_congr_ae, rw eventually_eq, rwa ae_restrict_iff' hs, }
+
 /-- Monotone convergence theorem -- sometimes called Beppo-Levi convergence.
 
 See `lintegral_supr_directed` for a more general form. -/
@@ -1735,6 +1740,10 @@ begin
   { rwa pairwise_disjoint_on_bool }
 end
 
+lemma lintegral_add_compl (f : α → ℝ≥0∞) {A : set α} (hA : measurable_set A) :
+  ∫⁻ x in A, f x ∂μ + ∫⁻ x in Aᶜ, f x ∂μ = ∫⁻ x, f x ∂μ :=
+by rw [← lintegral_add_measure, measure.restrict_add_restrict_compl hA]
+
 lemma lintegral_map [measurable_space β] {f : β → ℝ≥0∞} {g : α → β}
   (hf : measurable f) (hg : measurable g) : ∫⁻ a, f a ∂(map g μ) = ∫⁻ a, f (g a) ∂μ :=
 begin

src/measure_theory/integral/set_integral.lean

@@ -87,6 +87,89 @@ lemma integral_add_compl (hs : measurable_set s) (hfi : integrable f μ) :
 by rw [← integral_union (@disjoint_compl_right (set α) _ _) hs hs.compl
     hfi.integrable_on hfi.integrable_on, union_compl_self, integral_univ]
 
+lemma set_integral_eq_zero_of_forall_eq_zero {f : α → E} (hf : measurable f)
+  (ht_eq : ∀ x ∈ t, f x = 0) :
+  ∫ x in t, f x ∂μ = 0 :=
+begin
+  refine integral_eq_zero_of_ae _,
+  rw [eventually_eq, ae_restrict_iff (measurable_set_eq_fun hf measurable_zero)],
+  refine eventually_of_forall (λ x hx, _),
+  rw pi.zero_apply,
+  exact ht_eq x hx,
+end
+
+private lemma set_integral_union_eq_left_of_disjoint {f : α → E} (hf : measurable f)
+  (hfi : integrable f μ) (hs : measurable_set s) (ht : measurable_set t) (ht_eq : ∀ x ∈ t, f x = 0)
+  (hs_disj : disjoint s t) :
+  ∫ x in (s ∪ t), f x ∂μ = ∫ x in s, f x ∂μ :=
+by rw [integral_union hs_disj hs ht hfi.integrable_on hfi.integrable_on,
+  set_integral_eq_zero_of_forall_eq_zero hf ht_eq, add_zero]
+
+lemma set_integral_union_eq_left {f : α → E} (hf : measurable f) (hfi : integrable f μ)
+  (hs : measurable_set s) (ht : measurable_set t) (ht_eq : ∀ x ∈ t, f x = 0) :
+  ∫ x in (s ∪ t), f x ∂μ = ∫ x in s, f x ∂μ :=
+begin
+  let s_ := s \ {x | f x = 0},
+  have hs_ : measurable_set s_, from hs.diff (measurable_set_eq_fun hf measurable_const),
+  let s0 := s ∩ {x | f x = 0},
+  have hs0 : measurable_set s0, from hs.inter (measurable_set_eq_fun hf measurable_const),
+  have hs0_eq : ∀ x ∈ s0, f x = 0,
+    by { intros x hx, simp_rw [s0, set.mem_inter_iff] at hx, exact hx.2, },
+  have h_s_union : s = s_ ∪ s0, from (set.diff_union_inter s _).symm,
+  have h_s_disj : disjoint s_ s0,
+    from (@disjoint_sdiff_self_left (set α) {x | f x = 0} s _).mono_right
+      (set.inter_subset_right _ _),
+  rw [h_s_union, set_integral_union_eq_left_of_disjoint hf hfi hs_ hs0 hs0_eq h_s_disj],
+  have hst0_eq : ∀ x ∈ s0 ∪ t, f x = 0,
+  { intros x hx,
+    rw set.mem_union at hx,
+    cases hx,
+    { exact hs0_eq x hx, },
+    { exact ht_eq x hx, }, },
+  have hst_disj : disjoint s_ (s0 ∪ t),
+  { rw [← set.sup_eq_union, disjoint_sup_right],
+    exact ⟨h_s_disj, (@disjoint_sdiff_self_left (set α) {x | f x = 0} s _).mono_right ht_eq⟩, },
+  rw set.union_assoc,
+  exact set_integral_union_eq_left_of_disjoint hf hfi hs_ (hs0.union ht) hst0_eq hst_disj,
+end
+
+lemma set_integral_neg_eq_set_integral_nonpos [linear_order E] [order_closed_topology E]
+  {f : α → E} (hf : measurable f) (hfi : integrable f μ) :
+  ∫ x in {x | f x < 0}, f x ∂μ = ∫ x in {x | f x ≤ 0}, f x ∂μ :=
+begin
+  have h_union : {x | f x ≤ 0} = {x | f x < 0} ∪ {x | f x = 0},
+    by { ext, simp_rw [set.mem_union_eq, set.mem_set_of_eq], exact le_iff_lt_or_eq, },
+  rw h_union,
+  exact (set_integral_union_eq_left hf hfi (measurable_set_lt hf measurable_const)
+    (measurable_set_eq_fun hf measurable_const) (λ x hx, hx)).symm,
+end
+
+lemma integral_norm_eq_pos_sub_neg {f : α → ℝ} (hf : measurable f) (hfi : integrable f μ) :
+  ∫ x, ∥f x∥ ∂μ = ∫ x in {x | 0 ≤ f x}, f x ∂μ - ∫ x in {x | f x ≤ 0}, f x ∂μ :=
+have h_meas : measurable_set {x | 0 ≤ f x}, from measurable_set_le measurable_const hf,
+calc ∫ x, ∥f x∥ ∂μ = ∫ x in {x | 0 ≤ f x}, ∥f x∥ ∂μ + ∫ x in {x | 0 ≤ f x}ᶜ, ∥f x∥ ∂μ :
+  by rw ← integral_add_compl h_meas hfi.norm
+... = ∫ x in {x | 0 ≤ f x}, f x ∂μ + ∫ x in {x | 0 ≤ f x}ᶜ, ∥f x∥ ∂μ :
+begin
+  congr' 1,
+  refine set_integral_congr h_meas (λ x hx, _),
+  dsimp only,
+  rw [real.norm_eq_abs, abs_eq_self.mpr _],
+  exact hx,
+end
+... = ∫ x in {x | 0 ≤ f x}, f x ∂μ - ∫ x in {x | 0 ≤ f x}ᶜ, f x ∂μ :
+begin
+  congr' 1,
+  rw ← integral_neg,
+  refine set_integral_congr h_meas.compl (λ x hx, _),
+  dsimp only,
+  rw [real.norm_eq_abs, abs_eq_neg_self.mpr _],
+  rw [set.mem_compl_iff, set.nmem_set_of_eq] at hx,
+  linarith,
+end
+... = ∫ x in {x | 0 ≤ f x}, f x ∂μ - ∫ x in {x | f x ≤ 0}, f x ∂μ :
+by { rw ← set_integral_neg_eq_set_integral_nonpos hf hfi, congr, ext1 x, simp, }
+
 /-- For a function `f` and a measurable set `s`, the integral of `indicator s f`
 over the whole space is equal to `∫ x in s, f x ∂μ` defined as `∫ x, f x ∂(μ.restrict s)`. -/
 lemma integral_indicator (hs : measurable_set s) :
@@ -235,6 +318,24 @@ lemma set_integral_nonneg (hs : measurable_set s) (hf : ∀ a, a ∈ s → 0 ≤
   (0:ℝ) ≤ (∫ a in s, f a ∂μ) :=
 set_integral_nonneg_of_ae_restrict ((ae_restrict_iff' hs).mpr (ae_of_all μ hf))
 
+lemma set_integral_le_nonneg {s : set α} (hs : measurable_set s) (hf : measurable f)
+  (hfi : integrable f μ) :
+  ∫ x in s, f x ∂μ ≤ ∫ x in {y | 0 ≤ f y}, f x ∂μ :=
+begin
+  rw [← integral_indicator hs, ← integral_indicator (measurable_set_le measurable_const hf)],
+  exact integral_mono (hfi.indicator hs) (hfi.indicator (measurable_set_le measurable_const hf))
+    (indicator_le_indicator_nonneg s f),
+end
+
+lemma set_integral_nonpos_le {s : set α} (hs : measurable_set s) {f : α → ℝ} (hf : measurable f)
+  (hfi : integrable f μ) :
+  ∫ x in {y | f y ≤ 0}, f x ∂μ ≤ ∫ x in s, f x ∂μ :=
+begin
+  rw [← integral_indicator hs, ← integral_indicator (measurable_set_le hf measurable_const)],
+  exact integral_mono (hfi.indicator (measurable_set_le hf measurable_const)) (hfi.indicator hs)
+    (indicator_nonpos_le_indicator s f),
+end
+
 end nonneg
 
 lemma set_integral_mono_set {α : Type*} [measurable_space α] {μ : measure α}

src/measure_theory/measurable_space_def.lean

@@ -404,6 +404,8 @@ open measurable_space
 def measurable [measurable_space α] [measurable_space β] (f : α → β) : Prop :=
 ∀ ⦃t : set β⦄, measurable_set t → measurable_set (f ⁻¹' t)
 
+localized "notation `measurable[` m `]` := @measurable _ _ m _" in measure_theory
+
 variables [measurable_space α] [measurable_space β] [measurable_space γ]
 
 lemma measurable_id : measurable (@id α) := λ t, id