Skip to content

Commit 5869ccb

Browse files
committed
chore(Probability): split Independence.Kernel (#32327)
Create a new folder `Kernel` with two files: `Indep` is about independence of families of sets and sigma-algebras, while `IndepFun` contains the definitions and results about independence of random variables.
1 parent 169d847 commit 5869ccb

File tree

5 files changed

+753
-716
lines changed

5 files changed

+753
-716
lines changed

Mathlib.lean

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5633,7 +5633,8 @@ public import Mathlib.Probability.Independence.Conditional
56335633
public import Mathlib.Probability.Independence.InfinitePi
56345634
public import Mathlib.Probability.Independence.Integrable
56355635
public import Mathlib.Probability.Independence.Integration
5636-
public import Mathlib.Probability.Independence.Kernel
5636+
public import Mathlib.Probability.Independence.Kernel.Indep
5637+
public import Mathlib.Probability.Independence.Kernel.IndepFun
56375638
public import Mathlib.Probability.Independence.Process
56385639
public import Mathlib.Probability.Independence.ZeroOne
56395640
public import Mathlib.Probability.Integration

Mathlib/Probability/Independence/Basic.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@ Authors: Rémy Degenne
55
-/
66
module
77

8-
public import Mathlib.Probability.Independence.Kernel
8+
public import Mathlib.Probability.Independence.Kernel.IndepFun
99
public import Mathlib.MeasureTheory.Constructions.Pi
1010
public import Mathlib.MeasureTheory.Group.Convolution
1111

Mathlib/Probability/Independence/Conditional.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@ Authors: Rémy Degenne
55
-/
66
module
77

8-
public import Mathlib.Probability.Independence.Kernel
8+
public import Mathlib.Probability.Independence.Kernel.IndepFun
99
public import Mathlib.Probability.Kernel.CompProdEqIff
1010
public import Mathlib.Probability.Kernel.Composition.Lemmas
1111
public import Mathlib.Probability.Kernel.Condexp

0 commit comments

Comments
 (0)