test with a pfr chapter

blueprint/src/chapter/jensen.tex

@@ -0,0 +1,28 @@
+\chapter{Applications of Jensen's inequality}
+
+In this chapter, $h$ denotes the function $h(x) := x \log \frac{1}{x}$ for $x \in [0,1]$.
+
+\begin{lemma}[Concavity]\label{concave}
+  \lean{Real.strictConcaveOn_negMulLog}\leanok
+  $h$ is strictly concave on $[0,1]$.
+\end{lemma}
+
+\begin{proof} \leanok Check that $h'$ is strictly monotone decreasing.
+\end{proof}
+
+\begin{lemma}[Jensen]\label{jensen}
+  \lean{Real.sum_negMulLog_le} \leanok
+  If $S$ is a finite set, and $\sum_{s \in S} w_s = 1$ for some non-negative $w_s$, and $p_s \in [0,1]$ for all $s \in S$, then
+  $$ \sum_{s \in S} w_s h(p_s) \leq h(\sum_{s \in S} w_s p_s).$$
+\end{lemma}
+
+\begin{proof} \uses{concave}\leanok Apply Jensen and Lemma \ref{concave}.
+\end{proof}
+
+\begin{lemma}[Converse Jensen]\label{converse-jensen}
+  \lean{Real.sum_negMulLog_eq}\leanok
+If equality holds in the above lemma, then $p_s = \sum_{s \in S} w_s h(p_s)$ whenever $w_s \neq 0$.
+\end{lemma}
+
+\begin{proof} \uses{concave}\leanok Need some converse form of Jensen, not sure if it is already in Mathlib.  May also wish to state it as an if and only if.
+\end{proof}

blueprint/src/chapter/main.tex

@@ -2,4 +2,4 @@
 % Add chapters of the blueprint here.
 % This file is not meant to be built. Build src/web.tex or src/print.text instead.
 
-%\input{chapter/jensen}
+\input{chapter/jensen}