From 9227565f21d36c39befa55598a6c58522d1af0dc Mon Sep 17 00:00:00 2001
From: Bokuan Li <bokuan.li@mail.mcgill.ca>
Date: Sat, 20 Jun 2026 10:28:50 -0400
Subject: [PATCH] Added translation properties for Haar.

---
 src/measure/lcg/haar.tex | 51 ++++++++++++++++++++++++++++++++++++++++
 1 file changed, 51 insertions(+)

diff --git a/src/measure/lcg/haar.tex b/src/measure/lcg/haar.tex
index 4b5a8b0..ed6f0f0 100644
--- a/src/measure/lcg/haar.tex
+++ b/src/measure/lcg/haar.tex
@@ -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}