Skip to content

Commit a3b98ba

Browse files
RemyDegenneRemyDegenne
committed
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.
1 parent 56d44fc commit a3b98ba

4 files changed

Lines changed: 219 additions & 494 deletions

File tree

‎Mathlib/Probability/ConditionalExpectation.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -49,6 +49,7 @@ theorem condexp_indep_eq (hle₁ : m₁ ≤ m) (hle₂ : m₂ ≤ m) [SigmaFinit
4949
refine' Memℒp.induction_stronglyMeasurable hle₁ ENNReal.one_ne_top _ _ _ _ hfint _
5050
· exact ⟨f, hf, EventuallyEq.rfl⟩
5151
· intro c t hmt _
52+
rw [Indep_iff] at hindp
5253
rw [integral_indicator (hle₁ _ hmt), set_integral_const, smul_smul, ← ENNReal.toReal_mul,
5354
mul_comm, ← hindp _ _ hmt hms, set_integral_indicator (hle₁ _ hmt), set_integral_const,
5455
Set.inter_comm]

0 commit comments

Comments
 (0)