feat(probability/integration): characterize indep_fun by expected pro…

…duct of comp (#13270)

This is the third PR into probability/integration, to characterize independence by the expected product of compositions.

src/algebra/indicator_function.lean

@@ -420,6 +420,10 @@ section mul_zero_one_class
 
 variables [mul_zero_one_class M]
 
+lemma inter_indicator_one {s t : set α} :
+  (s ∩ t).indicator (1 : _ → M) = s.indicator 1 * t.indicator 1 :=
+funext (λ _, by simpa only [← inter_indicator_mul, pi.mul_apply, pi.one_apply, one_mul])
+
 lemma indicator_prod_one {s : set α} {t : set β} {x : α} {y : β} :
   (s ×ˢ t : set _).indicator (1 : _ → M) (x, y) = s.indicator 1 x * t.indicator 1 y :=
 by simp [indicator, ← ite_and]

src/measure_theory/integral/set_integral.lean

@@ -258,6 +258,11 @@ lemma integral_indicator_const (e : E) ⦃s : set α⦄ (s_meas : measurable_set
   ∫ (a : α), s.indicator (λ (x : α), e) a ∂μ = (μ s).to_real • e :=
 by rw [integral_indicator s_meas, ← set_integral_const]
 
+@[simp]
+lemma integral_indicator_one ⦃s : set α⦄ (hs : measurable_set s) :
+  ∫ a, s.indicator 1 a ∂μ = (μ s).to_real :=
+(integral_indicator_const 1 hs).trans ((smul_eq_mul _).trans (mul_one _))
+
 lemma set_integral_indicator_const_Lp {p : ℝ≥0∞} (hs : measurable_set s) (ht : measurable_set t)
   (hμt : μ t ≠ ∞) (x : E) :
   ∫ a in s, indicator_const_Lp p ht hμt x a ∂μ = (μ (t ∩ s)).to_real • x :=

src/probability/integration.lean

@@ -1,9 +1,9 @@
 /-
 Copyright (c) 2021 Martin Zinkevich. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Martin Zinkevich
+Authors: Martin Zinkevich, Vincent Beffara
 -/
-import measure_theory.integral.bochner
+import measure_theory.integral.set_integral
 import probability.independence
 
 /-!
@@ -235,4 +235,26 @@ begin
   ring
 end
 
+/-- Independence of functions `f` and `g` into arbitrary types is characterized by the relation
+  `E[(φ ∘ f) * (ψ ∘ g)] = E[φ ∘ f] * E[ψ ∘ g]` for all measurable `φ` and `ψ` with values in `ℝ`
+  satisfying appropriate integrability conditions. -/
+theorem indep_fun_iff_integral_comp_mul [is_finite_measure μ]
+  {β β' : Type*} {mβ : measurable_space β} {mβ' : measurable_space β'}
+  {f : α → β} {g : α → β'} {hfm : measurable f} {hgm : measurable g} :
+  indep_fun f g μ ↔
+  ∀ {φ : β → ℝ} {ψ : β' → ℝ},
+    measurable φ → measurable ψ → integrable (φ ∘ f) μ → integrable (ψ ∘ g) μ →
+    integral μ ((φ ∘ f) * (ψ ∘ g)) = integral μ (φ ∘ f) * integral μ (ψ ∘ g) :=
+begin
+  refine ⟨λ hfg _ _ hφ hψ, indep_fun.integral_mul_of_integrable (hfg.comp hφ hψ), _⟩,
+  rintro h _ _ ⟨A, hA, rfl⟩ ⟨B, hB, rfl⟩,
+  specialize h (measurable_one.indicator hA) (measurable_one.indicator hB)
+    ((integrable_const 1).indicator (hfm.comp measurable_id hA))
+    ((integrable_const 1).indicator (hgm.comp measurable_id hB)),
+  rwa [← ennreal.to_real_eq_to_real (measure_ne_top μ _), ennreal.to_real_mul,
+    ← integral_indicator_one ((hfm hA).inter (hgm hB)), ← integral_indicator_one (hfm hA),
+    ← integral_indicator_one (hgm hB), set.inter_indicator_one],
+  exact ennreal.mul_ne_top (measure_ne_top μ _) (measure_ne_top μ _)
+end
+
 end probability_theory