From 9504125410b3ea4f8f24c0e24bccd4511ac8cd46 Mon Sep 17 00:00:00 2001
From: Bokuan Li <bokuan.li@mail.mcgill.ca>
Date: Thu, 18 Jun 2026 21:00:12 -0400
Subject: [PATCH] Added uniqueness of Haar.

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

diff --git a/src/measure/lcg/haar.tex b/src/measure/lcg/haar.tex
index af86eb9..e68d3dc 100644
--- a/src/measure/lcg/haar.tex
+++ b/src/measure/lcg/haar.tex
@@ -145,7 +145,58 @@
         \item[(LH)] For each $f \in C_c(G)$ and $x \in G$, $I(L_xf) = I(f)$. 
     \end{enumerate}
     
-    By (i) and the \hyperref[Riesz Representation Theorem]{theorem:riesz-radon}, there exists a unique non-zero Radon measure $\mu: \cb_G \to [0, \infty]$ such that for each $f \in C_c^+(G)$, $I(f) = \int_G f d\mu$. Finally, by \hyperref[density of $C_c(\mu; \real)$ in $L^1(\mu; \real)$]{proposition:radon-cc-dense} and (LH), $\mu$ is a left Haar measure. 
+    By (i) and the \hyperref[Riesz Representation Theorem]{theorem:riesz-radon}, there exists a unique non-zero Radon measure $\mu: \cb_G \to [0, \infty]$ such that for each $f \in C_c^+(G)$, $I(f) = \int_G f d\mu$. Finally, by \hyperref[density of $C_c(G; \real)$ in $L^1(\mu; \real)$]{proposition:radon-cc-dense} and (LH), $\mu$ is a left Haar measure. 
+
+    (2): Let $f, g \in C_c^+(G) \setminus \bracs{0}$ and $\eps > 0$, then by \autoref{proposition:lcg-cc-uc}, there exists a symmetric neighbourhood $V \in \cn_G(1)$ such that for any $x \in G$ and $y \in V$, 
+    \[
+    |f(xy) - f(yx)|, |g(xy) - g(yx)| < \eps
+    \]
+
+    By \hyperref[Urysohn's lemma]{lemma:lch-urysohn}, there exists $h \in C_c^+(V) \setminus \bracs{0}$ such that $h(x) = h(x^{-1})$ for all $x \in V$. Since $f$ and $h$ are both compactly supported and $\mu, \nu$ are locally finite, by \hyperref[Tonelli's Theorem]{theorem:fubini-tonelli},
+    \begin{align*}
+        \paren{\int f d\mu}\paren{\int h d\nu} &= \iint f(x)h(y) \mu(dx)\nu(dy) \\
+        &= \iint f(yx)h(y) \nu(dx)\mu(dy) \\
+    \end{align*}
+
+    Similarly, by symmetry of $h$, 
+    \begin{align*}
+        \paren{\int h d\mu}\paren{\int f d\nu} &= \iint h(x)f(y) \mu(dx)\nu(dy) \\
+        &= \iint h(y^{-1}x)f(y) \mu(dx)\nu(dy) \\
+        &= \iint h(x^{-1}y)f(y) \nu(dy)\mu(dx) \\
+        &= \iint h(y)f(xy) \nu(dy)\mu(dx) \\
+        &= \iint h(y)f(xy) \mu(dx)\nu(dy)
+    \end{align*}
+
+    Thus there exists $C > 0$ such that
+    \begin{align*}
+    &\abs{\paren{\int f d\mu}\paren{\int h d\nu} - \paren{\int h d\mu}\paren{\int f d\nu}} \\ 
+    &\le \abs{\iint h(y)[f(xy) - f(yx)]\mu(dx)\nu(dy)} \le C\eps
+    \end{align*}
+
+    and
+    \[
+    \abs{\paren{\int g d\mu}\paren{\int h d\nu} - \paren{\int h d\mu}\paren{\int g d\nu}}
+    \le C\eps
+    \]
+
+    so there exists $C' > 0$ such that
+    \[
+    \abs{\frac{\int h d\nu}{\int h d\mu} - \frac{\int g d\nu}{\int g d\mu}}
+    \le C'\eps
+    \]
+
+    and
+    \[
+    \abs{\frac{\int f d\nu}{\int f d\mu} + \frac{\int h d\nu}{\int h d\mu}}
+    \le C'\eps
+    \]
+
+    Therefore
+    \[
+    \abs{\frac{\int f d\nu}{\int f d\mu} - \frac{\int g d\nu}{\int g d\mu}} \le 2C' \eps
+    \]
+
+    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}