Fix docs

leanprover-community · Oct 6, 2023 · 1414cd1 · 1414cd1
1 parent 1356d2f
commit 1414cd1
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 4 deletions.
diff --git a/docs/overview.yaml b/docs/overview.yaml
@@ -366,14 +366,14 @@ Probability Theory:
     conditional probability: 'ProbabilityTheory.cond'
     conditional expectation: 'MeasureTheory.condexp'
   Random variables and their laws:
-    discrete law: 'Pmf'
+    discrete law: 'PMF'
     probability density function: 'MeasureTheory.HasPDF'
     variance of a real-valued random variable: 'ProbabilityTheory.variance'
     independence of random variables: 'ProbabilityTheory.iIndepFun'
     Kolmogorov's $0$-$1$ law: 'ProbabilityTheory.measure_zero_or_one_of_measurableSet_limsup_atTop'
     mean of product of independent random variables: 'ProbabilityTheory.IndepFun.integral_mul_of_integrable'
     moment of a random variable: 'ProbabilityTheory.moment'
-    Bernoulli law: 'Pmf.bernoulli'
+    Bernoulli law: 'PMF.bernoulli'
   Convergence of a sequence of random variables:
     convergence in probability: 'MeasureTheory.TendstoInMeasure'
     $\mathrm{L}^p$ convergence: 'MeasureTheory.Lp'

diff --git a/docs/undergrad.yaml b/docs/undergrad.yaml
@@ -549,7 +549,7 @@ Probability Theory:
     conditional probability: 'ProbabilityTheory.cond'
     law of total probability: ''
   Random variables and their laws:
-    discrete law: 'Pmf'
+    discrete law: 'PMF'
     absolute continuity of probability laws: ''
     probability density function: 'MeasureTheory.HasPDF'
     law of joint probability: ''
@@ -558,7 +558,7 @@ Probability Theory:
     variance of a real-valued random variable: 'ProbabilityTheory.variance'
     transfer theorem: ''
     moments: 'ProbabilityTheory.moment'
-    Bernoulli law: 'Pmf.bernoulli'
+    Bernoulli law: 'PMF.bernoulli'
     binomial law: ''
     geometric law: ''
     Poisson law: ''