feat(probability/moments): mgf/cgf of a sum of independent random var…

…iables (#15140)




Co-authored-by: Rémy Degenne <remydegenne@gmail.com>

src/probability/independence.lean

@@ -630,6 +630,85 @@ begin
     rw [h_sets_s'_univ hi, set.univ_inter], },
 end
 
+lemma Indep_fun.indep_fun_prod [is_probability_measure μ]
+  {ι : Type*} {β : ι → Type*} {m : Π i, measurable_space (β i)}
+  {f : Π i, α → β i} (hf_Indep : Indep_fun m f μ) (hf_meas : ∀ i, measurable (f i))
+  (i j k : ι) (hik : i ≠ k) (hjk : j ≠ k) :
+  indep_fun (λ a, (f i a, f j a)) (f k) μ :=
+begin
+  classical,
+  have h_right : f k = (λ p : (Π j : ({k} : finset ι), β j), p ⟨k, finset.mem_singleton_self k⟩)
+    ∘ (λ a (j : ({k} : finset ι)), f j a) := rfl,
+  have h_meas_right : measurable
+      (λ p : (Π j : ({k} : finset ι), β j), p ⟨k, finset.mem_singleton_self k⟩),
+    from measurable_pi_apply ⟨k, finset.mem_singleton_self k⟩,
+  let s : finset ι := {i, j},
+  have h_left : (λ ω, (f i ω, f j ω))
+    = (λ p : (Π l : s, β l), (p ⟨i, finset.mem_insert_self i _⟩,
+        p ⟨j, finset.mem_insert_of_mem (finset.mem_singleton_self _)⟩))
+      ∘ (λ a (j : s), f j a),
+  { ext1 a,
+    simp only [prod.mk.inj_iff],
+    split; refl, },
+  have h_meas_left : measurable (λ p : (Π l : s, β l), (p ⟨i, finset.mem_insert_self i _⟩,
+      p ⟨j, finset.mem_insert_of_mem (finset.mem_singleton_self _)⟩)),
+    from measurable.prod (measurable_pi_apply ⟨i, finset.mem_insert_self i {j}⟩)
+      (measurable_pi_apply ⟨j, finset.mem_insert_of_mem (finset.mem_singleton_self j)⟩),
+  rw [h_left, h_right],
+  refine (hf_Indep.indep_fun_finset s {k} _ hf_meas).comp h_meas_left h_meas_right,
+  intros x hx,
+  simp only [finset.inf_eq_inter, finset.mem_inter, finset.mem_insert, finset.mem_singleton] at hx,
+  simp only [finset.bot_eq_empty, finset.not_mem_empty],
+  cases hx.1 with hx_eq hx_eq; rw hx_eq at hx,
+  { exact hik hx.2, },
+  { exact hjk hx.2, },
+end
+
+@[to_additive]
+lemma Indep_fun.mul [is_probability_measure μ]
+  {ι : Type*} {β : Type*} {m : measurable_space β} [has_mul β] [has_measurable_mul₂ β]
+  {f : ι → α → β} (hf_Indep : Indep_fun (λ _, m) f μ) (hf_meas : ∀ i, measurable (f i))
+  (i j k : ι) (hik : i ≠ k) (hjk : j ≠ k) :
+  indep_fun (f i * f j) (f k) μ :=
+begin
+  have : indep_fun (λ ω, (f i ω, f j ω)) (f k) μ := hf_Indep.indep_fun_prod hf_meas i j k hik hjk,
+  change indep_fun ((λ p : β × β, p.fst * p.snd) ∘ (λ ω, (f i ω, f j ω))) (id ∘ (f k)) μ,
+  exact indep_fun.comp this (measurable_fst.mul measurable_snd) measurable_id,
+end
+
+@[to_additive]
+lemma Indep_fun.indep_fun_finset_prod_of_not_mem [is_probability_measure μ]
+  {ι : Type*} {β : Type*} {m : measurable_space β} [comm_monoid β] [has_measurable_mul₂ β]
+  {f : ι → α → β} (hf_Indep : Indep_fun (λ _, m) f μ) (hf_meas : ∀ i, measurable (f i))
+  {s : finset ι} {i : ι} (hi : i ∉ s) :
+  indep_fun (∏ j in s, f j) (f i) μ :=
+begin
+  classical,
+  have h_right : f i = (λ p : (Π j : ({i} : finset ι), β), p ⟨i, finset.mem_singleton_self i⟩)
+    ∘ (λ a (j : ({i} : finset ι)), f j a) := rfl,
+  have h_meas_right : measurable
+      (λ p : (Π j : ({i} : finset ι), β), p ⟨i, finset.mem_singleton_self i⟩),
+    from measurable_pi_apply ⟨i, finset.mem_singleton_self i⟩,
+  have h_left : (∏ j in s, f j) = (λ p : (Π j : s, β), ∏ j, p j) ∘ (λ a (j : s), f j a),
+  { ext1 a,
+    simp only [function.comp_app],
+    have : (∏ (j : ↥s), f ↑j a) = (∏ (j : ↥s), f ↑j) a, by rw finset.prod_apply,
+    rw [this, finset.prod_coe_sort], },
+  have h_meas_left : measurable (λ p : (Π j : s, β), ∏ j, p j),
+    from finset.univ.measurable_prod (λ (j : ↥s) (H : j ∈ finset.univ), measurable_pi_apply j),
+  rw [h_left, h_right],
+  exact (hf_Indep.indep_fun_finset s {i} (finset.disjoint_singleton_left.mpr hi).symm hf_meas).comp
+    h_meas_left h_meas_right,
+end
+
+@[to_additive]
+lemma Indep_fun.indep_fun_prod_range_succ [is_probability_measure μ]
+  {β : Type*} {m : measurable_space β} [comm_monoid β] [has_measurable_mul₂ β]
+  {f : ℕ → α → β} (hf_Indep : Indep_fun (λ _, m) f μ) (hf_meas : ∀ i, measurable (f i))
+  (n : ℕ) :
+  indep_fun (∏ j in finset.range n, f j) (f n) μ :=
+hf_Indep.indep_fun_finset_prod_of_not_mem hf_meas finset.not_mem_range_self
+
 end indep_fun
 
 end probability_theory

src/probability/moments.lean

@@ -43,7 +43,7 @@ open_locale big_operators measure_theory probability_theory ennreal nnreal
 
 namespace probability_theory
 
-variables {Ω : Type*} {m : measurable_space Ω} {X : Ω → ℝ} {p : ℕ} {μ : measure Ω}
+variables {Ω ι : Type*} {m : measurable_space Ω} {X : Ω → ℝ} {p : ℕ} {μ : measure Ω}
 
 include m
 
@@ -182,16 +182,22 @@ by simp_rw [mgf, pi.neg_apply, mul_neg, neg_mul]
 
 lemma cgf_neg : cgf (-X) μ t = cgf X μ (-t) := by simp_rw [cgf, mgf_neg]
 
+/-- This is a trivial application of `indep_fun.comp` but it will come up frequently. -/
+lemma indep_fun.exp_mul {X Y : Ω → ℝ} (h_indep : indep_fun X Y μ) (s t : ℝ) :
+  indep_fun (λ ω, exp (s * X ω)) (λ ω, exp (t * Y ω)) μ :=
+begin
+  have h_meas : ∀ t, measurable (λ x, exp (t * x)) := λ t, (measurable_id'.const_mul t).exp,
+  change indep_fun ((λ x, exp (s * x)) ∘ X) ((λ x, exp (t * x)) ∘ Y) μ,
+  exact indep_fun.comp h_indep (h_meas s) (h_meas t),
+end
+
 lemma indep_fun.mgf_add {X Y : Ω → ℝ} (h_indep : indep_fun X Y μ)
   (h_int_X : integrable (λ ω, exp (t * X ω)) μ)
   (h_int_Y : integrable (λ ω, exp (t * Y ω)) μ) :
   mgf (X + Y) μ t = mgf X μ t * mgf Y μ t :=
 begin
   simp_rw [mgf, pi.add_apply, mul_add, exp_add],
-  refine indep_fun.integral_mul_of_integrable' _ h_int_X h_int_Y,
-  have h_meas : measurable (λ x, exp (t * x)) := (measurable_id'.const_mul t).exp,
-  change indep_fun ((λ x, exp (t * x)) ∘ X) ((λ x, exp (t * x)) ∘ Y) μ,
-  exact indep_fun.comp h_indep h_meas h_meas,
+  exact (h_indep.exp_mul t t).integral_mul_of_integrable' h_int_X h_int_Y,
 end
 
 lemma indep_fun.cgf_add {X Y : Ω → ℝ} (h_indep : indep_fun X Y μ)
@@ -205,6 +211,59 @@ begin
   exact log_mul (mgf_pos' hμ h_int_X).ne' (mgf_pos' hμ h_int_Y).ne',
 end
 
+lemma indep_fun.integrable_exp_mul_add {X Y : Ω → ℝ} (h_indep : indep_fun X Y μ)
+  (h_int_X : integrable (λ ω, exp (t * X ω)) μ)
+  (h_int_Y : integrable (λ ω, exp (t * Y ω)) μ) :
+  integrable (λ ω, exp (t * (X + Y) ω)) μ :=
+begin
+  simp_rw [pi.add_apply, mul_add, exp_add],
+  exact (h_indep.exp_mul t t).integrable_mul h_int_X h_int_Y,
+end
+
+lemma Indep_fun.integrable_exp_mul_sum [is_probability_measure μ]
+  {X : ι → Ω → ℝ} (h_indep : Indep_fun (λ i, infer_instance) X μ) (h_meas : ∀ i, measurable (X i))
+  {s : finset ι} (h_int : ∀ i ∈ s, integrable (λ ω, exp (t * X i ω)) μ) :
+  integrable (λ ω, exp (t * (∑ i in s, X i) ω)) μ :=
+begin
+  classical,
+  induction s using finset.induction_on with i s hi_notin_s h_rec h_int,
+  { simp only [pi.zero_apply, sum_apply, sum_empty, mul_zero, exp_zero],
+    exact integrable_const _, },
+  { have : ∀ (i : ι), i ∈ s → integrable (λ (ω : Ω), exp (t * X i ω)) μ,
+      from λ i hi, h_int i (mem_insert_of_mem hi),
+    specialize h_rec this,
+    rw sum_insert hi_notin_s,
+    refine indep_fun.integrable_exp_mul_add _ (h_int i (mem_insert_self _ _)) h_rec,
+    exact (h_indep.indep_fun_finset_sum_of_not_mem h_meas hi_notin_s).symm, },
+end
+
+lemma Indep_fun.mgf_sum [is_probability_measure μ]
+  {X : ι → Ω → ℝ} (h_indep : Indep_fun (λ i, infer_instance) X μ) (h_meas : ∀ i, measurable (X i))
+  {s : finset ι} (h_int : ∀ i ∈ s, integrable (λ ω, exp (t * X i ω)) μ) :
+  mgf (∑ i in s, X i) μ t = ∏ i in s, mgf (X i) μ t :=
+begin
+  classical,
+  induction s using finset.induction_on with i s hi_notin_s h_rec h_int,
+  { simp only [sum_empty, mgf_zero_fun, measure_univ, ennreal.one_to_real, prod_empty], },
+  { have h_int' : ∀ (i : ι), i ∈ s → integrable (λ (ω : Ω), exp (t * X i ω)) μ,
+      from λ i hi, h_int i (mem_insert_of_mem hi),
+    rw [sum_insert hi_notin_s, indep_fun.mgf_add
+        (h_indep.indep_fun_finset_sum_of_not_mem h_meas hi_notin_s).symm
+        (h_int i (mem_insert_self _ _)) (h_indep.integrable_exp_mul_sum h_meas h_int'),
+      h_rec h_int', prod_insert hi_notin_s], },
+end
+
+lemma Indep_fun.cgf_sum [is_probability_measure μ]
+  {X : ι → Ω → ℝ} (h_indep : Indep_fun (λ i, infer_instance) X μ) (h_meas : ∀ i, measurable (X i))
+  {s : finset ι} (h_int : ∀ i ∈ s, integrable (λ ω, exp (t * X i ω)) μ) :
+  cgf (∑ i in s, X i) μ t = ∑ i in s, cgf (X i) μ t :=
+begin
+  simp_rw cgf,
+  rw ← log_prod _ _ (λ j hj, _),
+  { rw h_indep.mgf_sum h_meas h_int, },
+  { exact (mgf_pos (h_int j hj)).ne', },
+end
+
 /-- **Chernoff bound** on the upper tail of a real random variable. -/
 lemma measure_ge_le_exp_mul_mgf [is_finite_measure μ] (ε : ℝ) (ht : 0 ≤ t)
   (h_int : integrable (λ ω, exp (t * X ω)) μ) :