refactor(Probability/Independence): define independence using kernel …

…independence (#6294) Independence is the special case of independence with respect to a kernel and a measure where the kernel is constant.
leanprover-community · Aug 2, 2023 · a3b98ba · a3b98ba
1 parent 56d44fc
commit a3b98ba
Show file tree

Hide file tree

Showing 4 changed files with 219 additions and 494 deletions.
diff --git a/Mathlib/Probability/ConditionalExpectation.lean b/Mathlib/Probability/ConditionalExpectation.lean
@@ -49,6 +49,7 @@ theorem condexp_indep_eq (hle₁ : m₁ ≤ m) (hle₂ : m₂ ≤ m) [SigmaFinit
   refine' Memℒp.induction_stronglyMeasurable hle₁ ENNReal.one_ne_top _ _ _ _ hfint _
   · exact ⟨f, hf, EventuallyEq.rfl⟩
   · intro c t hmt _
+    rw [Indep_iff] at hindp
     rw [integral_indicator (hle₁ _ hmt), set_integral_const, smul_smul, ← ENNReal.toReal_mul,
       mul_comm, ← hindp _ _ hmt hms, set_integral_indicator (hle₁ _ hmt), set_integral_const,
       Set.inter_comm]