From 8090f060d3f2a5c1c34350280aae822a1e816dfa Mon Sep 17 00:00:00 2001
From: Bokuan Li <bokuan.li@mail.mcgill.ca>
Date: Tue, 30 Jun 2026 14:13:58 -0400
Subject: [PATCH] Added local L^p spaces.

---
 src/fa/lp/index.tex |  1 +
 src/fa/lp/local.tex | 44 ++++++++++++++++++++++++++++++++++++++++++++
 2 files changed, 45 insertions(+)
 create mode 100644 src/fa/lp/local.tex

diff --git a/src/fa/lp/index.tex b/src/fa/lp/index.tex
index a13e9d9..e7dc003 100644
--- a/src/fa/lp/index.tex
+++ b/src/fa/lp/index.tex
@@ -6,3 +6,4 @@
 \input{./duality.tex}
 \input{./ui.tex}
 \input{./seq.tex}
+\input{./local.tex}
diff --git a/src/fa/lp/local.tex b/src/fa/lp/local.tex
new file mode 100644
index 0000000..f72ec68
--- /dev/null
+++ b/src/fa/lp/local.tex
@@ -0,0 +1,44 @@
+\section{Locally Integrable Functions}
+\label{section:locally-integrable}
+
+\begin{definition}[Locally Integrable*]
+\label{definition:locally-integrable}
+    Let $(X, \cm, \cf, \mu)$ be a \hyperref[scaffolded]{definition:measure-scaffold} measure space, $E$ be a normed vector space over $K \in \RC$, $f: X \to E$ be strongly measurable, and $p \in [1, \infty]$, then $f$ is \textbf{locally $p$-integrable} if for every $A \in \cf$, $\int_A \norm{f}_A^p d\mu < \infty$. 
+
+    The set $\mathcal{L}^p_\cf(X, \cm, \mu; E) = \mathcal{L}^p_\cf(X; E) = \mathcal{L}^p_\cf(\mu; E)$ is the space of all locally $p$-integrable $E$-valued functions on $X$. 
+\end{definition}
+
+\begin{definition}[Locally Bounded*]
+\label{definition:locally-bounded-measure}
+    Let $(X, \cm, \cf, \mu)$ be a \hyperref[scaffolded]{definition:measure-scaffold} measure space, $E$ be a normed vectorr space over $K \in \RC$, and $f: X \to E$ be strongly measurable, then $f$ is \textbf{essentially bounded} if for every $A \in \cf$, $\norm{\one_A f}_{L^\infty(A; E)} < \infty$. 
+
+    The set $\mathcal{L}^\infty_\cf(X, \cm, \mu; E) = \mathcal{L}^\infty_\cf(X; E) = \mathcal{L}^\infty_\cf(\mu; E)$ is the space of all locally bounded $E$-valued functions on $X$. 
+\end{definition}
+
+\begin{definition}[Local $L^p$ Space*]
+\label{definition:local-lp-space}
+    Let $(X, \cm, \cf, \mu)$ be a \hyperref[scaffolded]{definition:measure-scaffold} measure space, $E$ be a normed vector space over $K \in \RC$, and $p \in [1, \infty]$. For each $A \in \cf$ and $f \in \mathcal{L}^p_\cf(X, \cm, \mu; E)$, let $[f]_{L^p_A(X; \mu)} = \norm{\one_A f}_{L^p(X; \mu)}$, then the $[\cdot]_{L^p_A(X; \mu)}$ is a seminorm on \hyperref[$\mathcal{L}^p_\cf(X; E)$]{definition:locally-integrable}. The set
+    \[
+    L^p_\cf(X, \cm, \mu; E) = \mathcal{L}^p_\cf(X, \cm, \mu; E)/\bracs{f|f = 0\text{ a.e.}}
+    \]
+
+    equipped with the seminorms $\bracsn{[\cdot]_{L^p_A(X;\mu)}|A \in \cf}$ is a separated locally convex space, and the \textbf{local $L^p$ space} of $(X, \cm, \mu)$. 
+\end{definition}
+
+\begin{lemma}
+\label{lemma:gluing-local-lp}
+    Let $(X, \cm, \cf, \mu)$ be a \hyperref[scaffolded]{definition:measure-scaffold} localisable measure space, $E$ be a normed vector space over $K \in \RC$, $p \in [1, \infty]$, and $\bracsn{f_A}_{A \in \cf}$ such that:
+    \begin{enumerate}[label=(\alph*)]
+        \item For each $A \in \cf$, $f_A \in \mathcal{L}^p(A; E)$. 
+        \item For each $A, B \in \cf$, $f_A|_{A \cap B} = f_B|_{A \cap B}$ almost everywhere.
+        \item $\bigcup_{A \in \cf}f_A(A)$ is a separable subset of $E$. 
+    \end{enumerate}
+
+    then there exists a unique $f \in L^p_\cf(X; E)$ such that $f|_A = f_A$ for all $A \in \cf$. 
+\end{lemma}
+\begin{proof}
+    By the \hyperref[gluing lemma for measurable functions]{lemma:gluing-measurable}.
+\end{proof}
+
+
+