From a57b88618f43581d8626ac598b058d56a41edd3e Mon Sep 17 00:00:00 2001
From: Bokuan Li <bokuan.li@mail.mcgill.ca>
Date: Fri, 7 Aug 2026 20:14:39 -0400
Subject: [PATCH] Added existence of the weak integral.

---
 src/measure/weak-integral/definition.tex | 33 +++++++++++++++++++++---
 1 file changed, 29 insertions(+), 4 deletions(-)

diff --git a/src/measure/weak-integral/definition.tex b/src/measure/weak-integral/definition.tex
index aeb2a90..6ebad63 100644
--- a/src/measure/weak-integral/definition.tex
+++ b/src/measure/weak-integral/definition.tex
@@ -9,7 +9,7 @@
 As I know so little about weak integrals, I will Dunning-Kruger myself right now, give an opinion, and laugh about it later. My gripe with seeing the definition comes from the need to test against \textit{every} continuous linear functional. To me, this seems quite inflexible: consider integrating a distribution-valued function. \textit{Surely} it is wiser to only test this function against test functions rather than \textit{the dual of $\mathcal{D}'$ (dual with respect to $\mathcal{D}'$ with the bounded convergence topology)}. As such, it may be more productive to consider a more flexible form of testing, such as using duality. 
 
 
-\begin{definition}[Weakly Integrable*]
+\begin{definition}[Weak Integrability*]
 \label{definition:weakly-integrable}
     Let $(X, \cm, \mu)$ be a measure space, $\dpn{E, F}{\lambda}$ be a duality over $K \in \RC$, and $f: X \to E$, then $f$ is \textbf{Dunford $\lambda$-integrable*} if:
     \begin{enumerate}[label=(I\arabic*)]
@@ -29,7 +29,7 @@ As I know so little about weak integrals, I will Dunning-Kruger myself right now
     \begin{enumerate}
         \item[(I3+)] For each $A \in \cm$, the mapping
         \[
-        F \to K \quad \phi \mapsto \int_X \dpn{f(x), \phi}{\lambda} d\mu 
+        F \to K \quad \phi \mapsto \int_A \dpn{f(x), \phi}{\lambda} d\mu 
         \]
 
         is a $\sigma(F, E)$-continuous linear functional on $F$. 
@@ -43,9 +43,34 @@ It is at this point that I start to understand why the bidual setup is useful: e
 
 \begin{proposition}
 \label{proposition:dunford-existence}
-    Let 
+    Let $(X, \cm, \mu)$ be a measure space, $\dpn{E, F}{\lambda}$ be a duality over $K \in \RC$, and $f: X \to E$. If
+    \begin{enumerate}[label=(I\arabic*)]
+        \item $f$ is weakly measurable. 
+        \item For each $\phi \in F$, $\phi \circ f \in L^1(X; K)$.
+        \item[(C)] $F$ is a Fréchet space. 
+    \end{enumerate}
+
+    then $f$ is \hyperref[Dunford $\lambda$-integrable]{definition:weakly-integrable}. 
 \end{proposition}
-
+\begin{proof}[Proof, {{\cite[Section 3.3]{RyanTensor}}}. ]
+    Let $T: F \to L^1(X; K)$ be defined by $T\phi = \phi \circ f$. To see that $T$ is continuous, it is sufficient to apply the \hyperref[Closed Graph Theorem]{theorem:closed-graph}. 
+    
+    Let $\seq{\phi_n} \subset F$, $\phi \in F$, $\seq{g_n} \subset L^1(X; K)$, and $g \in L^1(X; K)$ such that
+    \begin{enumerate}[label=(\roman*)]
+        \item $g_n = \phi_n \circ f$ almost everywhere for all $n \in \natp$. 
+        \item $\phi_n \to \phi$ and $g_n \to g$ as $n \to \infty$.
+    \end{enumerate}
+    
+    
+    By passing through a subsequence using \autoref{theorem:cauchy-in-measure-limit}, assume further without loss of generality that $g_n \to g$ almost everywhere. In which case, $\phi_n \circ f \to g$ almost everywhere as well, and $\phi \circ f = g$ almost everywhere. Thus $T$ is continuous. 
+
+    Now, let $T^*: L^1(X; K)^* \to F^*$ be the adjoint of $T$. For each $A \in \cm$, the mapping $\Phi_A: L^1(X; K) \to K$ defined by $g \mapsto \int_A g d\mu$ is a continuous linear functional on $L^1(X; K)$. As such, for each $\phi \in F$, 
+    \[
+        \int_A \dpn{f, \phi}{\lambda} d\mu = \int_A T\phi d\mu = \dpn{T\phi, \Phi_A}{L^1(X; K)} = \dpn{\phi, T^*\Phi_A}{F}
+    \]
+
+    Therefore $T^*\Phi_A = \int_A^* f d\mu$ is the desired Dunford $\lambda$-integral of $f$ over $A$. 
+\end{proof}