chore(probability_theory/*): Rename folder (#11989)

Rename `probability_theory` to `probability`.
leanprover-community · Feb 15, 2022 · 4c76eac · 4c76eac
1 parent 430faa9
commit 4c76eac
Show file tree

Hide file tree

Showing 6 changed files with 4 additions and 5 deletions.
diff --git a/src/probability_theory/density.lean → src/probability/density.lean b/src/probability_theory/density.lean → src/probability/density.lean
diff --git a/src/probability_theory/independence.lean → src/probability/independence.lean b/src/probability_theory/independence.lean → src/probability/independence.lean
diff --git a/src/probability_theory/integration.lean → src/probability/integration.lean b/src/probability_theory/integration.lean → src/probability/integration.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Martin Zinkevich
 -/
 import measure_theory.integral.lebesgue
-import probability_theory.independence
+import probability.independence
 
 /-!
 # Integration in Probability Theory

diff --git a/src/probability_theory/martingale.lean → src/probability/martingale.lean b/src/probability_theory/martingale.lean → src/probability/martingale.lean
@@ -3,9 +3,8 @@ Copyright (c) 2021 Rémy Degenne. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Rémy Degenne, Kexing Ying
 -/
-
-import probability_theory.stopping
-import probability_theory.notation
+import probability.notation
+import probability.stopping
 
 /-!
 # Martingales
@@ -18,7 +17,7 @@ and for all `i ≤ j`, `μ[f j | ℱ.le i] ≤ᵐ[μ] f i`. Finally, `f : ι →
 submartingale with respect to the filtration `ℱ` if `f i` is integrable, `f` is adapted with
 resepct to `ℱ` and for all `i ≤ j`, `f i ≤ᵐ[μ] μ[f j | ℱ.le i]`.
 
-The definitions of filtration and adapted can be found in `probability_theory.stopping`.
+The definitions of filtration and adapted can be found in `probability.stopping`.
 
 ### Definitions
 

diff --git a/src/probability_theory/notation.lean → src/probability/notation.lean b/src/probability_theory/notation.lean → src/probability/notation.lean
diff --git a/src/probability_theory/stopping.lean → src/probability/stopping.lean b/src/probability_theory/stopping.lean → src/probability/stopping.lean