Merge pull request #83 from jstac/update-proof

Update: update domain from proof to prf for sphinx_proof

ctmc_lectures/ergodicity.md

@@ -192,14 +192,14 @@ The next result holds true under weaker conditions but the version stated here
 is easy to prove and sufficient for applications we consider.
 
 
-```{proof:theorem}
+```{prf:theorem}
 :label: statfromq
 
 Let $(P_t)$ be a UC Markov semigroup with generator $Q$.  A distribution
 $\psi$ on $S$ is stationary for $(P_t)$ if and only if $\psi Q = 0$.
 ```
 
-```{proof:proof}
+```{prf:proof}
 Fix $\psi \in \dD$ and suppose first that $\psi Q = 0$.
 
 Since $(P_t)$ is a UC Markov semigroup, we have $P_t = e^{tQ}$ for all $t$,
@@ -259,7 +259,7 @@ to $y$ if there exists a finite sequence $(z_i)_{i=0}^m$ in $S$ starting at
 $x=z_0$ and ending at $y=z_m$ such that $Q(z_i, z_{i+1}) > 0$ for all $i$.
 
 
-```{proof:theorem}
+```{prf:theorem}
 :label: equivirr
 
 Let $(P_t)$ be a UC Markov semigroup with generator $Q$.
@@ -271,7 +271,7 @@ For distinct states $x$ and $y$, the following statements are equivalent:
 ```
 
 
-```{proof:proof}
+```{prf:proof}
 Pick any two distinct states $x$ and $y$.
 
 It is obvious that statement 3 implies statement 1, so we need only prove 
@@ -318,7 +318,7 @@ $$
 
 
 Let $(Y_k)$ and $(J_k)$ be the embedded jump chain and jump sequence generated
-by {proof:ref}`ejc_algo`, with $Y_0 = u$.
+by {prf:ref}`ejc_algo`, with $Y_0 = u$.
 
 With $E_1 \sim \Exp(1)$ and $E_2 \sim \Exp(1)$, we have, for any $t > 0$,
 
@@ -352,9 +352,9 @@ $$
 
 ```
 
-{proof:ref}`equivirr` leads directly to the following strong result.
+{prf:ref}`equivirr` leads directly to the following strong result.
 
-```{proof:corollary}
+```{prf:corollary}
 :label: perimposs
 For a UC Markov semigroup $(P_t)$, the following statements are
 equivalent:
@@ -371,7 +371,7 @@ common to assume that the chain is aperiodic.
 This needs to be assumed on top of irreducibility if one wishes to rule out
 all dependence on initial conditions.
 
-{proof:ref}`perimposs` shows that periodicity is not a concern for irreducible
+{prf:ref}`perimposs` shows that periodicity is not a concern for irreducible
 continuous time Markov chains.
 
 Positive probability flow from $x$ to $y$ at some $t > 0$ immediately implies
@@ -427,7 +427,7 @@ Hence every Markov operator is contracting on $\dD$.
 
 Moreover, if $P$ is everywhere positive, then this inequality is strict:
 
-```{proof:lemma} Strict Contractivity
+```{prf:lemma} Strict Contractivity
 :label: strictcontract
 
 If $P$ is a Markov matrix and $P(x, y) > 0$ for all $x, y$, then 
@@ -452,29 +452,29 @@ Irreducibility of a given Markov chain implies that there are no disjoint
 
 This in turn leads to uniqueness of stationary distributions:
 
-```{proof:theorem}
+```{prf:theorem}
 :label: uniirr
 
 Let $(P_t)$ be a UC Markov semigroup on $S$.  If $(P_t)$ is irreducible, then
 $(P_t)$ has at most one stationary distribution.
 ```
 
 
-```{proof:proof}
+```{prf:proof}
 Suppose to the contrary that $\psi$ and $\phi$ are both stationary for
 $(P_t)$.
 
 Since $(P_t)$ is irreducible, we know that $P_1(x,y) > 0$ for all $x,y \in S$.
 
 If $\psi \not= \phi$, then, due to positivity of $P_1$, the strict inequality
-in {proof:ref}`strictcontract` holds.
+in {prf:ref}`strictcontract` holds.
 
 At the same time, by stationarity, $\| \psi P - \phi P \| = \| \psi - \phi
 \|$.  Contradiction.
 ```
 
 
-```{proof:example}
+```{prf:example}
 
 An M/M/1 queue with parameters $\mu, \lambda$ is a continuous time Markov chain $(X_t)$ on $S = \ZZ_+$ with with intensity matrix
 
@@ -496,7 +496,7 @@ If $\lambda$ and $\mu$ are both positive, then there is a $Q$-positive
 probability flow between any two states, in both directions, so the
 corresponding semigroup $(P_t)$ is irreducible.
 
-{proof:ref}`uniirr` now tells us that $(P_t)$ has at most one stationary
+{prf:ref}`uniirr` now tells us that $(P_t)$ has at most one stationary
 distribution.
 
 ```
@@ -515,7 +515,7 @@ The next result gives a connection between discrete and continuous stability.
 The critical ingredient linking these two concepts is the contractivity in
 {eq}`allmocontract`.
 
-```{proof:lemma}
+```{prf:lemma}
 :label: stabskel
 
 Let $(P_t)$ be a Markov semigroup. If there exists an $s > 0$ such that the
@@ -524,9 +524,9 @@ stable with the same stationary distribution.
 
 ```
 
-```{proof:proof}
+```{prf:proof}
 
-Let $(P_t)$ and $s$ be as in the statement of {proof:ref}`stabskel`.
+Let $(P_t)$ and $s$ be as in the statement of {prf:ref}`stabskel`.
 
 
 Let $\psi^*$ be the stationary distribution of $P_s$.  Fix $\psi \in \dD$ and 
@@ -561,11 +561,11 @@ The idea is to show that the state tends to drift back to a finite set over
 time.
 
 Such drift, when combined with the contractivity in
-{proof:ref}`strictcontract`, is enough to give global stability.
+{prf:ref}`strictcontract`, is enough to give global stability.
 
 The next theorem gives a useful version of this class of results.
 
-```{proof:theorem}
+```{prf:theorem}
 :label: sdrift
 
 Let $(P_t)$ be a UC Markov semigroup with intensity matrix $Q$.  If $(P_t)$ is
@@ -585,9 +585,9 @@ $$
 then $(P_t)$ is asymptotically stable.
 ```
 
-The proof of {proof:ref}`sdrift` can be found in {cite}`pichor2012stochastic`.
+The proof of {prf:ref}`sdrift` can be found in {cite}`pichor2012stochastic`.
 
-```{proof:example}
+```{prf:example}
 
 Consider again the M/M/1 queue on $\ZZ_+$ with intensity matrix {eq}`mm1q`.
 
@@ -596,7 +596,7 @@ Suppose that $\lambda < \mu$.
 It is intuitive that, in this case, the queue length will not 
 tend to infinity (since the service rate is higher than the arrival rate).
 
-This intuition can be confirmed via {proof:ref}`sdrift`, after setting $v(j) =
+This intuition can be confirmed via {prf:ref}`sdrift`, after setting $v(j) =
 j$.
 
 Indeed, we have, for any $i \geq 1$,
@@ -608,14 +608,14 @@ $$
 $$
 
 Setting $F=\{0\}$ and $M = \lambda - \mu = - \epsilon$, we see that the conditions
-of {proof:ref}`sdrift` hold.
+of {prf:ref}`sdrift` hold.
 
 Hence the associated semigroup $(P_t)$ is asymptotically stable.
 
 ```
 
 
-```{proof:corollary}
+```{prf:corollary}
 :label: sfinite
 
 If $(P_t)$ is an irreducible UC Markov semigroup and $S$ is finite, then
@@ -653,7 +653,7 @@ distribution.
 
 ### Exercise 3
 
-Confirm that {proof:ref}`sdrift` implies {proof:ref}`sfinite`.
+Confirm that {prf:ref}`sdrift` implies {prf:ref}`sfinite`.
 
 
 ## Solutions
@@ -696,5 +696,5 @@ $$
     = 0
 $$
 
-Hence the drift condition in {proof:ref}`sdrift` holds and $(P_t)$ is
+Hence the drift condition in {prf:ref}`sdrift` holds and $(P_t)$ is
 asymptotically stable.

ctmc_lectures/generators.md

@@ -210,12 +210,12 @@ $$
 (Convergence of operators is in operator norm.  If $\tau = 0$, then the limit
 $h \to 0$ in {eq}`devlim` is the right limit.)
 
-```{proof:example}
+```{prf:example}
 If $U_t = t V$ for some fixed $V \in \linop$, then it is easy to
 see that $V$ is the derivative of $t \mapsto U_t$ at every $t \in \RR_+$.
 ```
 
-```{proof:example}
+```{prf:example}
 In {doc}`our discussion <kolmogorov_fwd>` of the Kolmogorov forward equation 
 when $S$ is finite, we introduced the derivative of a map $t
 \mapsto P_t$, where each $P_t$ is a matrix on $S$.
@@ -229,7 +229,7 @@ hence pointwise and norm convergence coincide.
 
 Analogous to the matrix and scalar cases, we have the following result:
 
-```{proof:lemma} Differentiability of the Exponential Curve
+```{prf:lemma} Differentiability of the Exponential Curve
 :label: diffexpmap
 
 For all $A \in \linop$, the exponential curve $t \mapsto e^{tA}$ is everywhere differentiable and 
@@ -285,7 +285,7 @@ have, by definition of the operator norm,
 $\sup_{\| g \| \leq 1} \| U_s g - U_t g \| \to 0$ when $s \to t$.
 
 
-```{proof:example} Exponential curves are UC semigroups
+```{prf:example} Exponential curves are UC semigroups
 :label: ecuc
 
 If $U_t = e^{tA}$ for $t \in \RR_+$ and $A \in \linop$, then $(U_t)$
@@ -296,7 +296,7 @@ The claim that $(U_t)$ is an evolution semigroup follows directly from the
 properties of the exponential function given above.
 
 Uniform continuity can be established using arguments similar to those in the
-proof of differentiability in {proof:ref}`diffexpmap`. 
+proof of differentiability in {prf:ref}`diffexpmap`. 
 
 Since norm convergence on $\linop$ implies pointwise convergence, every
 uniformly continuous semigroup is a $C_0$ semigroup.
@@ -376,12 +376,12 @@ The next section gives details.
 
 ### A Characterization of Uniformly Continuous Semigroups
 
-We saw in {proof:ref}`ecuc` that exponential curves are an example
+We saw in {prf:ref}`ecuc` that exponential curves are an example
 of a UC semigroup.
 
 The next theorem tells us that there are no other examples.
 
-```{proof:theorem} UC Semigroups are Exponential Curves
+```{prf:theorem} UC Semigroups are Exponential Curves
 :label: ucsgec
 
 If $(U_t)$ is a UC semigroup on $\BB$, then there exists an $A \in \linop$
@@ -392,7 +392,7 @@ such that $U_t = e^{tA}$ for all $t \geq 0$.  Moreover,
 * $U_t' = A U_t = U_t A$ for all $t \geq 0$.
 ```
 
-The last three claims in {proof:ref}`ucsgec` follow directly from the
+The last three claims in {prf:ref}`ucsgec` follow directly from the
 first claim.
 
 The statement $U_t' = A U_t = U_t A$ is a
@@ -408,13 +408,13 @@ satisfying
 
 also satisfies $f(t) = e^{ta}$ for some $a \in \RR$.
 
-We proved something quite similar in {proof:ref}`exp_unique`, on 
+We proved something quite similar in {prf:ref}`exp_unique`, on 
 the memoryless property of the exponential function.
 
 For more discussion of the scalar case, see, for example,
 {cite}`sahoo2011introduction`.  
 
-For a full proof of the first claim in {proof:ref}`ucsgec`, in the setting of
+For a full proof of the first claim in {prf:ref}`ucsgec`, in the setting of
 a Banach algebra, see, for
 example, Chapter 7 of {cite}`bobrowski2005functional`.
 

ctmc_lectures/kolmogorov_bwd.md

@@ -108,7 +108,7 @@ Now we take $y$ as the new state for the process and repeat.
 
 Here is the same algorithm written more explicitly: 
 
-```{proof:algorithm} Jump Chain Algorithm
+```{prf:algorithm} Jump Chain Algorithm
 :label: ejc_algo
 
 **Inputs** $\psi \in \dD$, rate function $\lambda$, Markov matrix $K$
@@ -152,7 +152,7 @@ The differential equation in question has a special name:  the Kolmogorov backwa
 Here is the first step in the sequence listed above.
 
 
-```{proof:lemma} An Integral Equation
+```{prf:lemma} An Integral Equation
 
 The semigroup $(P_t)$ of the jump chain with rate function $\lambda$ and Markov matrix $K$ obeys the integral equation 
 
@@ -166,10 +166,10 @@ for all $t \geq 0$ and $x, y$ in $S$.
 ```
 
 Here $(P_t)$ is the Markov semigroup of $(X_t)$, the process constructed via
-{proof:ref}`ejc_algo`, while $K P_{t-\tau}$ is the matrix product of $K$ and
+{prf:ref}`ejc_algo`, while $K P_{t-\tau}$ is the matrix product of $K$ and
 $P_{t-\tau}$.
 
-```{proof:proof}
+```{prf:proof}
 
 Conditioning implicitly on $X_0 = x$, the semigroup $(P_t)$ must satisfy 
 
@@ -237,7 +237,7 @@ losing information by taking the time derivative.
 This leads to our main result for the lecture
 
 
-```{proof:theorem} Kolmogorov Backward Equation
+```{prf:theorem} Kolmogorov Backward Equation
 
 The semigroup $(P_t)$ of the jump chain with rate function $\lambda$ and Markov matrix $K$ satisfies the **Kolmogorov backward equation**
 
@@ -321,7 +321,7 @@ Let's investigate further the properties of the exponential solution.
 While we have confirmed that $P_t = e^{t Q}$ solves the Kolmogorov backward
 equation, we still need to check that this solution is a Markov semigroup.
 
-```{proof:lemma} From Jump Chain to Semigroup
+```{prf:lemma} From Jump Chain to Semigroup
 :label: jctosg
 
 Let $\lambda$ map $S$ to $\RR_+$ and let $K$ be a Markov matrix on $S$.
@@ -331,7 +331,7 @@ semigroup on $S$.
 ```
 
 
-```{proof:proof}
+```{prf:proof}
 Observe first that $Q$ has zero row sums, since
 
 $$

ctmc_lectures/kolmogorov_fwd.md

@@ -380,7 +380,7 @@ for all $t$?
 A square matrix $Q$ is called an **intensity matrix** if $Q$ has zero row
 sums and $Q(x, y) \geq 0$ whenever $x \not= y$.
 
-```{proof:theorem}
+```{prf:theorem}
 :label: intvsmk
 
 If $Q$ is a matrix on $S$ and $P_t := e^{tQ}$, then the following statements
@@ -390,10 +390,10 @@ are equivalent:
 1. $Q$ is an intensity matrix.
 ```
 
-The proof is related to that of {proof:ref}`jctosg` and is found as 
+The proof is related to that of {prf:ref}`jctosg` and is found as 
 a solved exercise below.
 
-```{proof:corollary}
+```{prf:corollary}
 :label: intvsmk_c
 
 If $Q$ is an intensity matrix on finite $S$ and $P_t = e^{tQ}$ for all $t \geq 0$,
@@ -410,7 +410,7 @@ some mild restrictions on $Q$.
 ## Jump Chains
 
 Let's return to the chain $(X_t)$ created from jump chain pair $(\lambda, K)$ in
-{proof:ref}`ejc_algo`.
+{prf:ref}`ejc_algo`.
 
 We found that the semigroup is given by 
 
@@ -523,7 +523,7 @@ Show that $Q$ is an intensity matrix and that {eq}`genfl` holds.
 
 ### Exercise 3 
 
-Prove {proof:ref}`intvsmk` by adapting the arguments in {proof:ref}`jctosg`.
+Prove {prf:ref}`intvsmk` by adapting the arguments in {prf:ref}`jctosg`.
 (This is nontrivial but worth at least trying.)
 
 Hint: The constant $m$ in the proof can be set to $\max_x |Q(x, x)|$.
@@ -586,7 +586,7 @@ $$
 
 Suppose that $Q$ is an intensity matrix, fix $t \geq 0$ and set $P_t = e^{tQ}$.
 
-The proof from {proof:ref}`jctosg` that $P_t$ has unit row sums applies
+The proof from {prf:ref}`jctosg` that $P_t$ has unit row sums applies
 directly to the current case.
 
 The proof of nonnegativity of $P_t$ can be applied after some