Added translation properties for Haar.

src/measure/lcg/haar.tex

@@ -119,7 +119,7 @@
 
     Thus $\mathcal{I}(f) = \bracs{I_g(f)|g \in C_c^+(G) \setminus \bracs{0}}$ is precompact for each $f \in C_c^+(G)$. 
 
-    For each $V \in \cn_G(1)$, let $E_V = \bracs{I_g|g \in C_c^+(V) \setminus \bracs{0}}$, then $\fF = \bracs{E_V|V \in \cn_G(1)}$ is a filter on the product space $\prod_{f \in C_c^+(G)}\ol{\mathcal{I}(f)}$. By \hyperref[Tychonoff's Theorem]{theorem:tychonoff}, $\bigcap_{V \in \cn_G(1)}\ol{E_V} \ne \emptyset$. 
+    For each $V \in \cn_G(1)$, let $E_V = \bracs{I_g|g \in C_c^+(V) \setminus \bracs{0}}$, then $\fF = \bracs{E_V|V \in \cn_G(1)}$ is a filter on the product space $\prod_{f \in C_c^+(G)}\ol{\mathcal{I}(f)}$. By \hyperref[Tychonoff's Theorem]{theorem:tychonoff}, $\prod_{f \in C_c^+(G)}\ol{\mathcal{I}(f)}$ is compact, and $\bigcap_{V \in \cn_G(1)}\ol{E_V} \ne \emptyset$. 
 
     Let $I \in \bigcap_{V \in \cn_G(1)}\ol{E_V}$, then by continuity, 
     \begin{enumerate}[label=(\roman*)]
@@ -199,5 +199,56 @@
     As the above holds for all $\eps > 0$, $\int f d\nu/\int f d\mu = \int g d\nu/\int g d\mu$. By uniqueness from the \hyperref[Riesz Representation Theorem]{section:riesz-radon}, there exists $\lambda > 0$ such that $\mu = \lambda \nu$. 
 \end{proof}
 
+\begin{proposition}
+\label{proposition:haar-measure-charge}
+    Let $G$ be a locally compact group and $\mu: \cb_G \to [0, \infty]$ be a left/right Haar measure, then:
+    \begin{enumerate}
+        \item For each $U \subset G$ open with $U \ne \emptyset$, $\mu(U) > 0$. 
+        \item For each $f \in C_c^+(G) \setminus \bracs{0}$, $\int \phi d\mu > 0$. 
+    \end{enumerate}
+\end{proposition}
+\begin{proof}[Proof, for left Haar measures. ]
+    Since $\mu \ne 0$, there exists $g \in C_c^+(G) \setminus \bracs{0}$ such that $\int g d\mu > 0$. By compactness of $\supp{g}$, there exists $\seqf{x_j} \subset G$ such that:
+    \[
+    \supp{g} \subset \bigcup_{j = 1}^n x_j^{-1}U \quad g \le \sum_{j = 1}^n L_{x_j}f
+    \]
+
+    Thus $0 < \int g d\mu \le n\mu(U)$ and $0 < \int g d\mu \le n \int f d\mu$. 
+\end{proof}
+
+\begin{proposition}
+\label{proposition:haar-translation}
+    Let $G$ be a locally compact group, $\mu: \cb_G \to [0, \infty]$ be a left Haar measure, $p \in [1, \infty)$, and $E$ be a normed vector space over $K \in \RC$, then the mapping
+    \[
+    G \times L^p(\mu; E) \quad (x, f) \mapsto L_xf
+    \]
+
+    is jointly continuous. Similarly, if $\nu: \cb_G \to [0, \infty]$ is a right Haar measure, then
+    \[
+    G \times L^p(\mu; E) \quad (x, f) \mapsto R_xf
+    \]
+
+    is also jointly continuous.
+\end{proposition}
+\begin{proof}[Proof of the left case. ]
+    Let $\eps > 0$, $x, y \in G$, and $f, g \in L^p(\mu; E)$, then
+    \begin{align*}
+        \norm{L_xf - L_yg}_{L^p(\mu; E)} &\le \norm{L_xf - L_yf}_{L^p(\mu; E)} + \norm{L_yf - L_y g}_{L^p(\mu; E)} \\
+        &= \norm{L_xf - L_yf}_{L^p(\mu; E)} + \norm{f - g}_{L^p(\mu; E)}
+    \end{align*}
+
+    By \autoref{proposition:radon-cc-dense}, there exists $\phi \in C_c(G)$ such that $\norm{\phi - f}_{L^p(\mu; E)} < \eps$. In which case, 
+    \begin{align*}
+        \norm{L_xf - L_yf}_{L^p(\mu; E)} &\le \norm{L_xf - L_x \phi}_{L^p(\mu; E)} + \norm{L_x\phi - L_y\phi}_{L^p(\mu; E)} \\
+        &+ \norm{L_yf - L_y \phi}_{L^p(\mu; E)} \\
+        &= 2\norm{f - \phi}_{L^p(\mu; E)} + \norm{L_x\phi - L_y\phi}_{L^p(\mu; E)} \\
+        &\le 2\eps + \normn{L_{x^{-1}y}\phi - \phi}_u\mu\bracs{\phi \ne 0}
+    \end{align*}
+
+    By \autoref{proposition:lcg-cc-uc}, there exists $V \in \cn_G(1)$ such that if $x^{-1}y \in V$, then $\norm{L_{x^{-1}y}\phi - \phi}_u < \eps/\mu\bracs{\phi \ne 0}$. Thus if $x^{-1}y \in V$, then
+    \[
+    \norm{L_xf - L_yf}_{L^p(\mu; E)} \le 3\eps + \norm{f - g}_{L^p(\mu; E)}
+    \]
+\end{proof}
 
 

src/measure/lebesgue-integral/non-negative.tex

@@ -5,10 +5,10 @@
 \label{definition:measurable-non-negative}
     Let $(X, \cm)$ be a measure space, then
     \[
-    \mathcal{L}^+(X, \cm) = \bracs{f: X \to \real| f \ge 0, f \text{ is } (\cm, \cb_\real) \text{-measurable}}
+    \mathcal{L}^+(X, \cm) = \bracs{f: X \to [0, \infty]| f \ge 0, f \text{ is } (\cm, \cb_\real) \text{-measurable}}
     \]
 
-    is the space of non-negative $\real$-valued measurable functions on $(X, \cm)$.
+    is the space of non-negative $\ol \real$-valued measurable functions on $(X, \cm)$.
 \end{definition}
 
 \begin{definition}[Integral of Non-Negative Function]
@@ -23,19 +23,36 @@
 
 \begin{lemma}
 \label{lemma:lebesgue-non-negative-strict}
-    Let $(X, \cm, \mu)$ be a measure space and $f \in \mathcal{L}^+(X, \cm)$, then
-    \[
-    \int f d\mu = \sup\bracs{\int \phi d\mu \bigg | \phi \in \Sigma^+(X, \cm), \phi|_{\bracs{f > 0}} < f|_{\bracs{f > 0}}, \phi \le f}
-    \]
+    Let $(X, \cm, \mu)$ be a measure space and $f \in \mathcal{L}^+(X, \cm)$. 
+    \begin{enumerate}
+        \item For each $\phi \in \Sigma^+(X, \cm)$, denote $\phi \le_u f$ if there exists $\delta > 0$ such that $\phi + \delta \ge f$ on $\bracs{\phi > 0}$, then
+        \[
+        \int f d\mu = \sup\bracs{\int \phi d\mu \bigg | \phi \in \Sigma^+(X, \cm), \phi \le_u f}
+        \]
 
+        \item If $\mu$ is semifinite, then
+        \[
+        \int f d\mu = \sup\bracs{\int \phi d\mu \bigg | \phi \in \Sigma^+(X, \cm) \cap L^1(X; \real), \phi \le_u f}
+        \]
+    \end{enumerate}
 \end{lemma}
 \begin{proof}
-    Let $\phi \in \Sigma^+(X, \cm)$ with $\phi \le f$, then for any $\alpha \in (0, 1)$, $\alpha \phi|_{\bracs{f > 0}} < f|_{\bracs{f > 0}}$. Since
+    (1): Let $\phi \in \Sigma^+(X, \cm)$ with $\phi \le f$ and $\alpha \in (0, 1)$. Since $\phi(X) \setminus \bracs{0} \subset (0, \infty)$ is finite, $\delta = \min_{y \in \phi(X) \setminus \bracs{0}}(1 - \alpha)y > 0$. Thus $\alpha \phi + \delta \le \phi \le f$ on $\bracs{\phi > 0} = \bracs{\alpha \phi > 0}$, and $\alpha \phi \le_u f$. 
+    
+    By \hyperref[linearity on simple functions]{proposition:lebesgue-simple-properties}, 
     \[
     \int \phi d\mu = \sup_{\alpha \in (0, 1)}\alpha \int \phi d\mu = \sup_{\alpha \in (0, 1)}\int \alpha \phi d\mu
     \]
 
-    the two sides are equal.
+    Thus
+    \[
+    \int \phi d\mu \le \sup\bracs{\int \psi d\mu \bigg | \psi \in \Sigma^+(X, \cm), \psi \le_u f}
+    \]
+
+    As the above holds for all $\phi \in \Sigma^+(X, \cm)$, 
+    \[
+    \int f d\mu = \sup\bracs{\int \psi d\mu \bigg | \psi \in \Sigma^+(X, \cm), \psi \le_u f}
+    \]
 \end{proof}
 
 \begin{theorem}[Monotone Convergence Theorem]
@@ -98,7 +115,7 @@
 \begin{proof}
     (1): By \autoref{lemma:lebesgue-simple-monotone}, there exists $\seq{f_n}, \seq{g_n} \subset \Sigma^+(X, \cm)$ with $0 \le f_n \le f$ and $0 \le g_n \le g$ for each $n \in \natp$, $f_n \upto f$, and $g_n \upto g$. By \autoref{proposition:lebesgue-simple-properties} and the \hyperref[Monotone Convergence Theorem]{theorem:mct},
     \begin{align*}
-    \int \alpha f + g d\mu = \limv{n}\int \alpha f_n + g_n d\mu = \alpha\limv{n}\int f_n d\mu + \limv{n}\int g_n d\mu \\
+    \int \alpha f + g d\mu &= \limv{n}\int \alpha f_n + g_n d\mu = \alpha\limv{n}\int f_n d\mu + \limv{n}\int g_n d\mu \\
     &= \alpha \int f d\mu + \int g d\mu
     \end{align*}
 

src/measure/lebesgue-integral/simple.tex

@@ -16,9 +16,9 @@
     is the \textbf{Lebesgue integral} of $f$.
 \end{definition}
 
-\begin{proposition}[{{\cite[Proposition 2.13]{Folland}}}]
+\begin{proposition}
 \label{proposition:lebesgue-simple-properties}
-    Let $(X, \cm, \mu)$ be a measure space and $f, g \in \Sigma^*(X, \cm)$, then:
+    Let $(X, \cm, \mu)$ be a measure space and $f, g \in \Sigma^+(X, \cm)$, then:
     \begin{enumerate}
         \item For any $\alpha \ge 0$, $\int \alpha f d\mu = \alpha \int f d\mu$.
         \item $\int f + g d\mu = \int f d\mu + \int g d\mu$.
@@ -26,7 +26,7 @@
         \item The mapping $A \mapsto \int \one_A \cdot f d\mu$ is a measure on $(X, \cm)$.
     \end{enumerate}
 \end{proposition}
-\begin{proof}
+\begin{proof}[Proof, {{\cite[Proposition 2.13]{Folland}}}. ]
     (1): If $\alpha = 0$, then $\int \alpha f d\mu = \int 0 d\mu = 0 = 0 \cdot \int f d\mu$. Otherwise, the mapping $y \mapsto \alpha y$ is a bijection. Hence
     \[
     \alpha f = \sum_{y \in f(X)} (\alpha y) \cdot \one_{\bracs{f = y}}

src/measure/measurable-maps/in-measure.tex

@@ -101,21 +101,34 @@
     \]
 \end{theorem}
 \begin{proof}
-    By \autoref{definition:lebesgue-non-negative}, $\int f_\alpha d\mu \le \int f d\mu$ for each $\alpha \in A$.
+    By \autoref{definition:lebesgue-non-negative}, $\int f_\alpha d\mu \le \int f d\mu$ for each $\alpha \in A$. 
 
-    Assume without loss of generality that $f \ne 0$. Let $\phi \in \Sigma^+(X, \cm)$ with $\phi|_{\bracs{f > 0}} < f|_{\bracs{f > 0}}$ and $\phi \le f$. Since $\mu$ is semifinite, assume further without loss of generality that $\phi \in L^1(X, \cm; \real)$ as well. 
-    
-    Let $\eps > 0$ and $\lambda \in (0, 1)$, then $\delta = \min_{y \in \phi(X) \setminus \bracs{0}}(1 - \lambda)y > 0$. By (b), there exists $\alpha \in A$ such that
+    On the other hand, using \autoref{lemma:lebesgue-non-negative-strict}, it is sufficient to show that
     \[
-    \mu\bracs{f_\alpha + \delta < f} < \frac{\epsilon}{\norm{\phi}_u}
+    \lim_{\alpha \in A}\int f_\alpha d\mu = \sup_{\alpha \in A}\int f_\alpha d\mu \ge \int \phi d\mu
+    \]
+    
+    for any $\phi \in \Sigma^+(X, \cm)$ satisfying:
+    \begin{enumerate}[label=(\roman*)]
+        \item There exists $\delta > 0$ such that $\phi + \delta \le f$ on $\bracs{\phi > 0}$. 
+        \item $\phi \in L^1(X, \cm)$. 
+    \end{enumerate}
+
+    To this end, let $\eps > 0$. Since $\mu\bracs{\phi > 0} < \infty$, by (b), there exists $\alpha \in A$ such that
+    \[
+    \mu\bracs{\phi > 0, f_\alpha + \delta < \phi} \le \mu\bracs{\phi > 0, f_\alpha + \delta < f} < \frac{\eps}{\norm{\phi}_u}
     \]
 
-    In which case, 
+    In which case, by \hyperref[linearity]{proposition:lebesgue-simple-properties},
     \begin{align*}
-        \int f_\alpha d\mu &\ge \int_{\bracs{f_\alpha + \delta \ge f}} f_\alpha d\mu \ge \int_{\bracs{f_\alpha + \delta \ge f}}\lambda\phi d\mu \\
-        &\ge \lambda\int \phi d\mu - \frac{\eps \norm{\phi}_u}{\norm{\phi}_u} = \lambda \int \phi d\mu - \eps
+        \int \phi d\mu &= \int_{\bracs{\phi > 0}}\phi d\mu = \int_{\bracs{\phi > 0, f_\alpha + \delta \ge \phi}} \phi d\mu + \int_{\bracs{\phi > 0, f_\alpha + \delta < \phi}} \phi d\mu \\
+        &\le \int_{\bracs{\phi > 0, f_\alpha + \delta \ge \phi}} f_\alpha d\mu +\norm{\phi}_u\mu \bracs{\phi > 0, f_\alpha + \delta < \phi} \\
+        &\le \int f_\alpha d\mu + \norm{\phi}_u \frac{\eps}{\norm{\phi}_u} = \int f_\alpha d\mu + \eps
     \end{align*}
 
-    As the above holds for all $\eps > 0$, $\lambda \in (0, 1)$, $\sup_{\alpha \in A}\int f_\alpha d\mu \ge \int \phi d\mu$. Therefore $\sup_{\alpha \in A}\int f_\alpha d\mu \ge \int f d\mu$ by \autoref{lemma:lebesgue-non-negative-strict}. 
+    As the above holds for all $\eps > 0$, $\int \phi d\mu \le \sup_{\alpha \in A}\int f_\alpha d\mu$. Therefore
+    \[
+    \int f d\mu = \sup_{\alpha \in A}\int f_\alpha d\mu = \lim_{\alpha \in A}\int f_\alpha d\mu
+    \]
 \end{proof}