feat(measure_theory/function/conditional_expectation/basic): add some…

… condexp lemmas (#16273)

src/measure_theory/function/conditional_expectation/basic.lean

@@ -2083,6 +2083,18 @@ begin
     ((condexp_ae_eq_condexp_L1 hm _).symm.add (condexp_ae_eq_condexp_L1 hm _).symm),
 end
 
+lemma condexp_finset_sum {ι : Type*} {s : finset ι} {f : ι → α → F'}
+  (hf : ∀ i ∈ s, integrable (f i) μ) :
+  μ[∑ i in s, f i | m] =ᵐ[μ] ∑ i in s, μ[f i | m] :=
+begin
+  induction s using finset.induction_on with i s his heq hf,
+  { rw [finset.sum_empty, finset.sum_empty, condexp_zero] },
+  { rw [finset.sum_insert his, finset.sum_insert his],
+    exact (condexp_add (hf i $ finset.mem_insert_self i s) $ integrable_finset_sum' _
+      (λ j hmem, hf j $ finset.mem_insert_of_mem hmem)).trans
+      ((eventually_eq.refl _ _).add (heq $ λ j hmem, hf j $ finset.mem_insert_of_mem hmem)) }
+end
+
 lemma condexp_smul (c : 𝕜) (f : α → F') : μ[c • f | m] =ᵐ[μ] c • μ[f|m] :=
 begin
   by_cases hm : m ≤ m0,
@@ -2142,6 +2154,26 @@ begin
     ((condexp_L1_mono hf hg hfg).trans_eq (condexp_ae_eq_condexp_L1 hm _).symm),
 end
 
+lemma condexp_nonneg {E} [normed_lattice_add_comm_group E] [complete_space E] [normed_space ℝ E]
+  [ordered_smul ℝ E] {f : α → E} (hf : 0 ≤ᵐ[μ] f) :
+  0 ≤ᵐ[μ] μ[f | m] :=
+begin
+  by_cases hfint : integrable f μ,
+  { rw (condexp_zero.symm : (0 : α → E) = μ[0 | m]),
+    exact condexp_mono (integrable_zero _ _ _) hfint hf },
+  { exact eventually_eq.le (condexp_undef hfint).symm }
+end
+
+lemma condexp_nonpos {E} [normed_lattice_add_comm_group E] [complete_space E] [normed_space ℝ E]
+  [ordered_smul ℝ E] {f : α → E} (hf : f ≤ᵐ[μ] 0) :
+  μ[f | m] ≤ᵐ[μ] 0 :=
+begin
+  by_cases hfint : integrable f μ,
+  { rw (condexp_zero.symm : (0 : α → E) = μ[0 | m]),
+    exact condexp_mono hfint (integrable_zero _ _ _) hf },
+  { exact eventually_eq.le (condexp_undef hfint) }
+end
+
 /-- **Lebesgue dominated convergence theorem**: sufficient conditions under which almost
   everywhere convergence of a sequence of functions implies the convergence of their image by
   `condexp_L1`. -/

src/topology/algebra/monoid.lean

@@ -6,6 +6,7 @@ Authors: Johannes Hölzl, Mario Carneiro
 import algebra.big_operators.finprod
 import data.set.pointwise
 import topology.algebra.mul_action
+import algebra.big_operators.pi
 
 /-!
 # Theory of topological monoids
@@ -500,6 +501,16 @@ lemma continuous_finset_prod {f : ι → X → M} (s : finset ι) :
   (∀ i ∈ s, continuous (f i)) → continuous (λa, ∏ i in s, f i a) :=
 continuous_multiset_prod _
 
+@[to_additive] lemma eventually_eq_prod {X M : Type*} [comm_monoid M]
+  {s : finset ι} {l : filter X} {f g : ι → X → M} (hs : ∀ i ∈ s, f i =ᶠ[l] g i) :
+  ∏ i in s, f i =ᶠ[l] ∏ i in s, g i :=
+begin
+  replace hs: ∀ᶠ x in l, ∀ i ∈ s, f i x = g i x,
+  { rwa eventually_all_finset },
+  filter_upwards [hs] with x hx,
+  simp only [finset.prod_apply, finset.prod_congr rfl hx],
+end
+
 open function
 
 @[to_additive]