From 5b04a8969716f310a27f13e36b48dc8f4ac8b220 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?R=C3=A9my=20Degenne?= Date: Wed, 1 Sep 2021 07:45:39 +0000 Subject: [PATCH] feat(measure_theory/conditional_expectation): the integral of the norm of the conditional expectation is lower (#8318) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 --- src/algebra/indicator_function.lean | 16 +++ .../function/conditional_expectation.lean | 59 ++++++++++ src/measure_theory/integral/bochner.lean | 9 ++ src/measure_theory/integral/lebesgue.lean | 9 ++ src/measure_theory/integral/set_integral.lean | 101 ++++++++++++++++++ src/measure_theory/measurable_space_def.lean | 2 + 6 files changed, 196 insertions(+) diff --git a/src/algebra/indicator_function.lean b/src/algebra/indicator_function.lean index 7b0b2702fa0e7..bf9fc5be61da6 100644 --- a/src/algebra/indicator_function.lean +++ b/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) diff --git a/src/measure_theory/function/conditional_expectation.lean b/src/measure_theory/function/conditional_expectation.lean index 0c4ae25b38ca7..363b3275943ff 100644 --- a/src/measure_theory/function/conditional_expectation.lean +++ b/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 diff --git a/src/measure_theory/integral/bochner.lean b/src/measure_theory/integral/bochner.lean index 177cd5b5d1959..d452717c4181e 100644 --- a/src/measure_theory/integral/bochner.lean +++ b/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 diff --git a/src/measure_theory/integral/lebesgue.lean b/src/measure_theory/integral/lebesgue.lean index 301d104e66b42..c490f79d59230 100644 --- a/src/measure_theory/integral/lebesgue.lean +++ b/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 diff --git a/src/measure_theory/integral/set_integral.lean b/src/measure_theory/integral/set_integral.lean index 79b1c7b345b71..ef507d23cd41f 100644 --- a/src/measure_theory/integral/set_integral.lean +++ b/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 α} diff --git a/src/measure_theory/measurable_space_def.lean b/src/measure_theory/measurable_space_def.lean index b7d688c5a87b1..ab7649d31b8cf 100644 --- a/src/measure_theory/measurable_space_def.lean +++ b/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