## Formalized Name Stability of Minimizing Movements under Gamma-Convergence ## Formalized Statement Let $(X,d)$ be a complete metric space. For each $k\in\mathbb N$, let $\mathcal E_k:X\to(-\infty,\infty]$ be a proper lower semicontinuous functional, and let $\mathcal E:X\to(-\infty,\infty]$ be a proper lower semicontinuous functional. Let $|\partial\mathcal E_k|:X\to[0,\infty]$ and $|\partial\mathcal E|:X\to[0,\infty]$ denote their metric slopes. Assume that there exists $M\in\mathbb R$ such that $\mathcal E_k[x]\ge M$ for every $k\in\mathbb N$ and every $x\in X$, and $\mathcal E[x]\ge M$ for every $x\in X$. Assume that, for every $\tau>0$ and every sequence $(z_k)_{k\in\mathbb N}\subset X$ with $z_k\to z$ in $X$, the functionals $F_{k,\tau,z_k}:X\to(-\infty,\infty]$ defined by \begin{align*} F_{k,\tau,z_k}(x):=\mathcal E_k[x]+\frac{1}{2\tau}d^2(x,z_k) \end{align*} Gamma-converge, with respect to the metric topology of $X$, to the functional $F_{\tau,z}:X\to(-\infty,\infty]$ defined by \begin{align*} F_{\tau,z}(x):=\mathcal E[x]+\frac{1}{2\tau}d^2(x,z). \end{align*} Assume the following compactness condition. For every $C>0$ and every $T>0$, there exists a compact set $K_{C,T}\subset X$ such that, whenever $k\in\mathbb N$, $\tau\in(0,T]$, $N\in\mathbb N$, $N\tau\le T$, and $x_0,\dots,x_N\in X$ satisfy \begin{align*} x_{j+1}\in\operatorname*{argmin}_{x\in X}\left\{\mathcal E_k[x]+\frac{1}{2\tau}d^2(x,x_j)\right\} \end{align*} for every $j\in\{0,\dots,N-1\}$, \begin{align*} \mathcal E_k[x_0]\le C, \end{align*} and \begin{align*} \sum_{j=0}^{N-1}\frac{d^2(x_{j+1},x_j)}{\tau}\le C, \end{align*} then $x_j\in K_{C,T}$ for every $j\in\{0,\dots,N\}$. Assume the Sandier--Serfaty lower semicontinuity condition: if $(k_n)_{n\in\mathbb N}\subset\mathbb N$ satisfies $k_n\to\infty$, if $(y_n)_{n\in\mathbb N}\subset X$ satisfies $y_n\to y$ in $X$, and if \begin{align*} \sup_{n\in\mathbb N}\mathcal E_{k_n}[y_n]<\infty \end{align*} and \begin{align*} \sup_{n\in\mathbb N}|\partial\mathcal E_{k_n}|(y_n)<\infty, \end{align*} then \begin{align*} \mathcal E[y]\le \liminf_{n\to\infty}\mathcal E_{k_n}[y_n] \end{align*} and \begin{align*} |\partial\mathcal E|(y)\le \liminf_{n\to\infty}|\partial\mathcal E_{k_n}|(y_n). \end{align*} Assume also that $|\partial\mathcal E|$ is a strong upper gradient for $\mathcal E$. Let $(\tau_k)_{k\in\mathbb N}\subset(0,\infty)$ satisfy $\tau_k\downarrow0$, and let $(x_{k,0})_{k\in\mathbb N}\subset X$ satisfy $x_{k,0}\to x_0$ in $X$ and \begin{align*} \mathcal E_k[x_{k,0}]\to\mathcal E[x_0]<\infty. \end{align*} For each $k\in\mathbb N$, assume that a sequence $(x_{k,j})_{j\ge0}\subset X$ exists and satisfies \begin{align*} x_{k,j+1}\in\operatorname*{argmin}_{x\in X}\left\{\mathcal E_k[x]+\frac{1}{2\tau_k}d^2(x,x_{k,j})\right\} \end{align*} for every $j\ge0$. Define $\bar x_k:[0,\infty)\to X$ by $\bar x_k(0):=x_{k,0}$ and, for $j\in\mathbb N$, by \begin{align*} \bar x_k(t):=x_{k,j}\qquad\text{for }(j-1)\tau_k<t\le j\tau_k. \end{align*} For $r\ge0$, define $\bar x_k(r-\tau_k):=x_{k,0}$ when $0\le r\le\tau_k$, and define it by the preceding interpolation when $r>\tau_k$. Assume in addition that the schemes admit discrete slope control in the following sense. For every $T>0$, there exist Borel maps $\tilde x_k:[0,T]\to X$ and Borel functions $g_k:[0,T]\to[0,\infty]$ such that \begin{align*} g_k(r)\ge |\partial\mathcal E_k|(\tilde x_k(r)) \end{align*} for $\mathcal L^1$-a.e. $r\in[0,T]$, \begin{align*} \lim_{k\to\infty}\sup_{0\le r\le T}d(\tilde x_k(r),\bar x_k(r))=0, \end{align*} and \begin{align*} \sup_{k\in\mathbb N}\mathcal E_k[\tilde x_k(r)]<\infty \end{align*} for $\mathcal L^1$-a.e. $r\in[0,T]$. Finally, assume that for every $T>0$ there is a sequence $\varepsilon_k(T)\to0$ such that, for every $0\le s\le t\le T$, \begin{align*} \mathcal E_k[\bar x_k(t)]+\frac12\int_s^t \left(\frac{d(\bar x_k(r),\bar x_k(r-\tau_k))}{\tau_k}\right)^2\,d\mathcal L^1(r)+\frac12\int_s^t g_k^2(r)\,d\mathcal L^1(r)\le \mathcal E_k[\bar x_k(s)]+\varepsilon_k(T). \end{align*} Then there exist a subsequence of $(k)_{k\in\mathbb N}$, not relabelled, and an absolutely continuous curve $x:[0,\infty)\to X$ such that, for every $T>0$, \begin{align*} \bar x_k(t)\to x(t) \end{align*} in $X$ for every $t\in[0,T]$. Moreover $x(0)=x_0$, and $x$ is a curve of maximal slope for $\mathcal E$ with respect to $|\partial\mathcal E|$: for every $0\le s\le t<\infty$, \begin{align*} \mathcal E[x(t)]+\frac12\int_s^t |x'|^2(r)\,d\mathcal L^1(r)+\frac12\int_s^t |\partial\mathcal E|^2(x(r))\,d\mathcal L^1(r)\le \mathcal E[x(s)]. \end{align*} ## Proof [proofplan] We first extract uniform bounds on the discrete action and slope terms from the assumed discrete energy-dissipation inequality. These bounds, together with the compactness hypothesis, give compactness of the piecewise-constant interpolations and an absolutely continuous limit curve. We then pass to the limit in the energy, metric-speed, and slope terms: Gamma-liminf gives the endpoint energy lower bound, weak lower semicontinuity gives the metric derivative bound, and the Sandier--Serfaty hypothesis gives the slope bound at almost every time. The final point is to replace the limiting right endpoint energy by $\mathcal E[x(s)]$; this follows from the discrete inequality on $[0,s]$ and the strong-upper-gradient inequality for the limiting curve. [/proofplan] [step:Derive uniform energy, action, and compactness bounds on finite intervals] Fix $T>0$. Define $N_k(T)\in\mathbb N\cup\{0\}$ by \begin{align*} N_k(T):=\max\{j\in\mathbb N\cup\{0\}:j\tau_k\le T\}. \end{align*} Define the discrete speed $a_k:[0,\infty)\to[0,\infty)$ by \begin{align*} a_k(r):=\frac{d(\bar x_k(r),\bar x_k(r-\tau_k))}{\tau_k}. \end{align*} The map $a_k$ is Borel because $\bar x_k$ is piecewise constant. Since $\mathcal E_k[x_{k,0}]\to\mathcal E[x_0]$, there are constants $C_0>0$ and $k_0\in\mathbb N$ such that \begin{align*} \mathcal E_k[x_{k,0}]\le C_0 \end{align*} for every $k\ge k_0$. Applying the assumed discrete energy-dissipation inequality with $s=0$ gives, for every $t\in[0,T]$ and every sufficiently large $k$, \begin{align*} \mathcal E_k[\bar x_k(t)]+\frac12\int_0^t a_k^2(r)\,d\mathcal L^1(r)+\frac12\int_0^t g_k^2(r)\,d\mathcal L^1(r)\le C_0+1. \end{align*} Using the lower bound $\mathcal E_k\ge M$, we obtain \begin{align*} \sup_{0\le t\le T}\mathcal E_k[\bar x_k(t)]\le C_0+1 \end{align*} and \begin{align*} \int_0^T a_k^2(r)\,d\mathcal L^1(r)+\int_0^T g_k^2(r)\,d\mathcal L^1(r)\le 2(C_0+1-M) \end{align*} for all sufficiently large $k$. Set \begin{align*} C_T:=2(C_0+1-M). \end{align*} Then \begin{align*} \int_0^T a_k^2(r)\,d\mathcal L^1(r)\le C_T \end{align*} and \begin{align*} \int_0^T g_k^2(r)\,d\mathcal L^1(r)\le C_T \end{align*} for all sufficiently large $k$. On each interval $((j-1)\tau_k,j\tau_k]$, the value of $a_k$ is $d(x_{k,j},x_{k,j-1})/\tau_k$. Hence \begin{align*} \int_0^{N\tau_k} a_k^2(r)\,d\mathcal L^1(r)=\sum_{j=0}^{N-1}\frac{d^2(x_{k,j+1},x_{k,j})}{\tau_k} \end{align*} whenever $N\in\mathbb N$. For all sufficiently large $k$, one has $\tau_k\le1$. If $0\le t\le T$, then $\bar x_k(t)$ is one of the nodes $x_{k,j}$ with $j\tau_k\le T+\tau_k\le T+1$. Applying the compactness hypothesis with time horizon $T+1$ and bound $C_{T+1}$ gives a compact set $K_T\subset X$ such that \begin{align*} \bar x_k(t)\in K_T \end{align*} for every $t\in[0,T]$ and all sufficiently large $k$. [/step] [step:Extract a pointwise limit curve and prove its absolute continuity] Fix $T>0$. For $0\le s\le t\le T$, the triangle inequality along the grid cells intersecting $[s,t]$ gives \begin{align*} d(\bar x_k(s),\bar x_k(t))\le \int_s^{\min\{t+\tau_k,T+1\}}a_k(r)\,d\mathcal L^1(r). \end{align*} Applying the Cauchy-Schwarz inequality in $L^2((s,\min\{t+\tau_k,T+1\}),\mathcal L^1)$ to $a_k$ and the constant function $1$, and using the bound on $[0,T+1]$, gives \begin{align*} d(\bar x_k(s),\bar x_k(t))\le C_{T+1}^{1/2}(t-s+\tau_k)^{1/2} \end{align*} for all sufficiently large $k$. [guided] Fix $T>0$. The compactness estimate says that the values of $\bar x_k$ on $[0,T]$ eventually lie in one compact subset of $X$. To turn compactness of values into compactness of curves, we need a uniform modulus of continuity up to the time-step error. For $0\le s\le t\le T$, the interpolation $\bar x_k$ can jump only when a grid point is crossed. Summing those jumps and using the triangle inequality gives \begin{align*} d(\bar x_k(s),\bar x_k(t))\le \int_s^{\min\{t+\tau_k,T+1\}}a_k(r)\,d\mathcal L^1(r). \end{align*} The upper endpoint is enlarged by one time step because $s$ and $t$ need not be grid points; for large $k$ this enlarged interval is contained in $[0,T+1]$. We now apply the Cauchy-Schwarz inequality on the measure space $((s,\min\{t+\tau_k,T+1\}),\mathcal L^1)$. The two functions are $a_k$ and the constant function $1$. Since $a_k\in L^2(0,T+1)$ by the previous step and the interval has finite Lebesgue measure, the hypotheses of Cauchy-Schwarz are satisfied. Therefore \begin{align*} \int_s^{\min\{t+\tau_k,T+1\}}a_k(r)\,d\mathcal L^1(r)\le \left(\int_s^{\min\{t+\tau_k,T+1\}}a_k^2(r)\,d\mathcal L^1(r)\right)^{1/2}(t-s+\tau_k)^{1/2}. \end{align*} The action bound on $[0,T+1]$ gives \begin{align*} \int_s^{\min\{t+\tau_k,T+1\}}a_k^2(r)\,d\mathcal L^1(r)\le C_{T+1}. \end{align*} Combining these estimates yields \begin{align*} d(\bar x_k(s),\bar x_k(t))\le C_{T+1}^{1/2}(t-s+\tau_k)^{1/2}. \end{align*} This estimate is the exact substitute for equicontinuity in the piecewise-constant setting: the extra $\tau_k$ disappears as $k\to\infty$. Let $D\subset[0,\infty)$ be a countable dense set containing $0$. For each fixed $T>0$, the set $D\cap[0,T]$ is countable and the values $\bar x_k(r)$ with $r\in D\cap[0,T]$ eventually lie in the compact set $K_T$. A diagonal subsequence therefore exists such that $\bar x_k(r)$ converges in $X$ for every $r\in D$. The modulus estimate makes the limit independent of the approximating sequence from $D$, so it extends uniquely to a map $x:[0,\infty)\to X$. Moreover, for every $t\in[0,T]$, \begin{align*} \bar x_k(t)\to x(t) \end{align*} in $X$. It remains to prove that $x$ is absolutely continuous. Since $(a_k)$ is bounded in $L^2((0,T),\mathcal L^1)$, the Banach-Alaoglu theorem and reflexivity of $L^2((0,T),\mathcal L^1)$ give a further subsequence and a function $a\in L^2((0,T),\mathcal L^1)$ such that \begin{align*} a_k\rightharpoonup a \end{align*} weakly in $L^2((0,T),\mathcal L^1)$. Fix $0\le \alpha\le\beta<T$. Define $\phi_k:(0,T)\to\mathbb R$ and $\phi:(0,T)\to\mathbb R$ by \begin{align*} \phi_k(r):=\mathbb 1_{(\alpha,\min\{\beta+\tau_k,T\})}(r) \end{align*} and \begin{align*} \phi(r):=\mathbb 1_{(\alpha,\beta)}(r). \end{align*} Then $\phi_k\to\phi$ strongly in $L^2((0,T),\mathcal L^1)$ because the symmetric difference of the two intervals has Lebesgue measure at most $\tau_k$. The uniform $L^2$ bound on $(a_k)$ gives \begin{align*} \left|\int_0^T a_k(r)(\phi_k(r)-\phi(r))\,d\mathcal L^1(r)\right|\le \|a_k\|_{L^2(0,T)}\|\phi_k-\phi\|_{L^2(0,T)}\to0. \end{align*} Weak convergence against the fixed test function $\phi$ gives \begin{align*} \int_0^T a_k(r)\phi(r)\,d\mathcal L^1(r)\to\int_0^T a(r)\phi(r)\,d\mathcal L^1(r). \end{align*} Passing to the limit in the distance estimate yields \begin{align*} d(x(\alpha),x(\beta))\le \int_\alpha^\beta a(r)\,d\mathcal L^1(r). \end{align*} This is the metric characterization of absolute continuity on $[0,T]$, with $a\in L^2(0,T)\subset L^1(0,T)$. Hence $x$ is absolutely continuous on $[0,T]$. [/guided] Let $D\subset[0,\infty)$ be a countable dense set containing $0$. By compactness of the values on $D\cap[0,T]$ and a diagonal argument over increasing integer time horizons, there is a subsequence such that $\bar x_k(r)$ converges in $X$ for every $r\in D$. The preceding modulus estimate extends the limit uniquely to a curve $x:[0,\infty)\to X$ and gives \begin{align*} \bar x_k(t)\to x(t) \end{align*} for every $t\in[0,T]$ and every $T>0$. Since $(a_k)$ is bounded in $L^2((0,T),\mathcal L^1)$, after passing to a further subsequence there exists $a\in L^2((0,T),\mathcal L^1)$ such that \begin{align*} a_k\rightharpoonup a \end{align*} weakly in $L^2((0,T),\mathcal L^1)$. For fixed $0\le s\le t<T$, define $\phi_k:(0,T)\to\mathbb R$ and $\phi:(0,T)\to\mathbb R$ by \begin{align*} \phi_k(r):=\mathbb 1_{(s,\min\{t+\tau_k,T\})}(r) \end{align*} and \begin{align*} \phi(r):=\mathbb 1_{(s,t)}(r). \end{align*} Then $\phi_k\to\phi$ strongly in $L^2((0,T),\mathcal L^1)$. The uniform $L^2$ bound on $(a_k)$ gives \begin{align*} \int_0^T a_k(r)\phi_k(r)\,d\mathcal L^1(r)-\int_0^T a_k(r)\phi(r)\,d\mathcal L^1(r)\to0. \end{align*} Weak convergence against $\phi$ gives \begin{align*} \int_0^T a_k(r)\phi(r)\,d\mathcal L^1(r)\to\int_0^T a(r)\phi(r)\,d\mathcal L^1(r). \end{align*} Therefore \begin{align*} d(x(s),x(t))\le \int_s^t a(r)\,d\mathcal L^1(r). \end{align*} Thus $x$ is absolutely continuous on $[0,T]$. Since $T>0$ was arbitrary, $x$ is absolutely continuous on every compact subinterval of $[0,\infty)$. The convergence at $0$ and the hypothesis $x_{k,0}\to x_0$ give $x(0)=x_0$. [/step] [step:Pass to the lower limit in the endpoint energy] We first derive the unpenalized Gamma-liminf consequence. Let $(y_k)_{k\in\mathbb N}\subset X$ and $y\in X$ satisfy $y_k\to y$ in $X$. Fix $\tau>0$ and define $z_k:=y$ for every $k\in\mathbb N$. The Gamma-liminf inequality for $F_{k,\tau,z_k}$ gives \begin{align*} \mathcal E[y]\le \liminf_{k\to\infty}\left(\mathcal E_k[y_k]+\frac{1}{2\tau}d^2(y_k,y)\right). \end{align*} Since $d(y_k,y)\to0$, it follows that \begin{align*} \mathcal E[y]\le \liminf_{k\to\infty}\mathcal E_k[y_k]. \end{align*} Applying this with $y_k=\bar x_k(t)$ and $y=x(t)$ gives, for every fixed $t\ge0$, \begin{align*} \mathcal E[x(t)]\le \liminf_{k\to\infty}\mathcal E_k[\bar x_k(t)]. \end{align*} At $t=0$, the assumed convergence of initial energies gives \begin{align*} \mathcal E[x(0)]=\lim_{k\to\infty}\mathcal E_k[x_{k,0}]. \end{align*} [/step] [step:Pass to the lower limit in the metric derivative term] Fix $0\le s\le t\le T$. Let $a\in L^2((0,T),\mathcal L^1)$ be the weak limit obtained in the compactness step. Since \begin{align*} d(x(\alpha),x(\beta))\le \int_\alpha^\beta a(r)\,d\mathcal L^1(r) \end{align*} for every $0\le\alpha\le\beta\le T$, the definition of the metric derivative of an absolutely continuous curve implies \begin{align*} |x'|(r)\le a(r) \end{align*} for $\mathcal L^1$-a.e. $r\in[0,T]$. Therefore \begin{align*} \int_s^t |x'|^2(r)\,d\mathcal L^1(r)\le \int_s^t a^2(r)\,d\mathcal L^1(r). \end{align*} The squared norm is weakly lower semicontinuous in $L^2((s,t),\mathcal L^1)$, so \begin{align*} \int_s^t a^2(r)\,d\mathcal L^1(r)\le \liminf_{k\to\infty}\int_s^t a_k^2(r)\,d\mathcal L^1(r). \end{align*} Hence \begin{align*} \int_s^t |x'|^2(r)\,d\mathcal L^1(r)\le \liminf_{k\to\infty}\int_s^t a_k^2(r)\,d\mathcal L^1(r). \end{align*} [/step] [step:Pass to the lower limit in the slope term] Fix $T>0$. Since $(g_k)$ is bounded in $L^2((0,T),\mathcal L^1)$, after passing to a further subsequence there exists $g\in L^2((0,T),\mathcal L^1)$ such that \begin{align*} g_k\rightharpoonup g \end{align*} weakly in $L^2((0,T),\mathcal L^1)$. By Mazur's lemma applied in the Banach space $L^2((0,T),\mathcal L^1)$, there are integers $N_m\ge m$ and coefficients $\alpha_{m,k}\in[0,1]$, for $m\le k\le N_m$, such that \begin{align*} \sum_{k=m}^{N_m}\alpha_{m,k}=1 \end{align*} and the convex combinations $h_m:[0,T]\to[0,\infty]$ defined by \begin{align*} h_m(r):=\sum_{k=m}^{N_m}\alpha_{m,k}g_k(r) \end{align*} satisfy $h_m\to g$ strongly in $L^2((0,T),\mathcal L^1)$. Passing to a subsequence in $m$, we may assume that \begin{align*} h_m(r)\to g(r) \end{align*} for $\mathcal L^1$-a.e. $r\in[0,T]$. Let $A\subset[0,T]$ be the full-measure set of all $r$ such that $h_m(r)\to g(r)$, $g_k(r)\ge |\partial\mathcal E_k|(\tilde x_k(r))$ for every $k$ after modifying the functions on null sets, and \begin{align*} \sup_{k\in\mathbb N}\mathcal E_k[\tilde x_k(r)]<\infty. \end{align*} Fix $r\in A$. The uniform closeness of $\tilde x_k$ to $\bar x_k$ and the pointwise convergence of $\bar x_k(r)$ imply \begin{align*} \tilde x_k(r)\to x(r) \end{align*} in $X$. We claim that \begin{align*} |\partial\mathcal E|(x(r))\le \liminf_{k\to\infty}g_k(r). \end{align*} If the right-hand side is infinite, there is nothing to prove. Otherwise choose a subsequence $(k_n)_{n\in\mathbb N}$ realizing the finite liminf, so that $g_{k_n}(r)$ is bounded and \begin{align*} \lim_{n\to\infty}g_{k_n}(r)=\liminf_{k\to\infty}g_k(r). \end{align*} Since \begin{align*} |\partial\mathcal E_{k_n}|(\tilde x_{k_n}(r))\le g_{k_n}(r), \end{align*} the slopes along this subsequence are uniformly bounded. The Sandier--Serfaty lower semicontinuity hypothesis applies to $y_n:=\tilde x_{k_n}(r)$ and $y:=x(r)$, because $\tilde x_{k_n}(r)\to x(r)$, the energies are uniformly bounded by the definition of $A$, and the slopes are uniformly bounded. Therefore \begin{align*} |\partial\mathcal E|(x(r))\le \liminf_{n\to\infty}|\partial\mathcal E_{k_n}|(\tilde x_{k_n}(r))\le \lim_{n\to\infty}g_{k_n}(r). \end{align*} This proves the claim. From the claim, for every $\varepsilon>0$ there exists $m_0\in\mathbb N$ such that \begin{align*} g_k(r)\ge |\partial\mathcal E|(x(r))-\varepsilon \end{align*} for every $k\ge m_0$. Therefore, for $m\ge m_0$, \begin{align*} h_m(r)\ge |\partial\mathcal E|(x(r))-\varepsilon. \end{align*} Letting $m\to\infty$ and then $\varepsilon\downarrow0$ gives \begin{align*} |\partial\mathcal E|(x(r))\le g(r) \end{align*} for every $r\in A$. Hence this inequality holds for $\mathcal L^1$-a.e. $r\in[0,T]$. Consequently, \begin{align*} \int_s^t |\partial\mathcal E|^2(x(r))\,d\mathcal L^1(r)\le \int_s^t g^2(r)\,d\mathcal L^1(r). \end{align*} By weak lower semicontinuity of the squared $L^2((s,t),\mathcal L^1)$ norm, \begin{align*} \int_s^t g^2(r)\,d\mathcal L^1(r)\le \liminf_{k\to\infty}\int_s^t g_k^2(r)\,d\mathcal L^1(r). \end{align*} Thus \begin{align*} \int_s^t |\partial\mathcal E|^2(x(r))\,d\mathcal L^1(r)\le \liminf_{k\to\infty}\int_s^t g_k^2(r)\,d\mathcal L^1(r). \end{align*} [/step] [step:Identify the limiting right endpoint energy] Fix $0\le s\le T$. Applying the discrete energy-dissipation inequality on $[0,s]$ gives \begin{align*} \mathcal E_k[\bar x_k(s)]+\frac12\int_0^s a_k^2(r)\,d\mathcal L^1(r)+\frac12\int_0^s g_k^2(r)\,d\mathcal L^1(r)\le \mathcal E_k[x_{k,0}]+\varepsilon_k(T). \end{align*} Taking the upper limit and using the convergence of the initial energies yields \begin{align*} \limsup_{k\to\infty}\mathcal E_k[\bar x_k(s)]\le \mathcal E[x(0)]-\liminf_{k\to\infty}\left(\frac12\int_0^s a_k^2(r)\,d\mathcal L^1(r)+\frac12\int_0^s g_k^2(r)\,d\mathcal L^1(r)\right). \end{align*} The superadditivity of $\liminf$ for two sequences bounded from below gives \begin{align*} \liminf_{k\to\infty}\left(\frac12\int_0^s a_k^2(r)\,d\mathcal L^1(r)+\frac12\int_0^s g_k^2(r)\,d\mathcal L^1(r)\right)\ge \frac12\liminf_{k\to\infty}\int_0^s a_k^2(r)\,d\mathcal L^1(r)+\frac12\liminf_{k\to\infty}\int_0^s g_k^2(r)\,d\mathcal L^1(r). \end{align*} Using the lower semicontinuity estimates for the metric derivative and the slope term on $[0,s]$, we obtain \begin{align*} \limsup_{k\to\infty}\mathcal E_k[\bar x_k(s)]\le \mathcal E[x(0)]-\frac12\int_0^s |x'|^2(r)\,d\mathcal L^1(r)-\frac12\int_0^s |\partial\mathcal E|^2(x(r))\,d\mathcal L^1(r). \end{align*} Since $|\partial\mathcal E|$ is a strong upper gradient for $\mathcal E$ and $x$ is absolutely continuous, the map $r\mapsto\mathcal E[x(r)]$ has an absolutely continuous representative on $[0,s]$ and satisfies \begin{align*} \mathcal E[x(0)]-\mathcal E[x(s)]\le \int_0^s |\partial\mathcal E|(x(r))|x'|(r)\,d\mathcal L^1(r). \end{align*} Young's inequality $ab\le a^2/2+b^2/2$, applied with $a=|\partial\mathcal E|(x(r))$ and $b=|x'|(r)$, gives \begin{align*} \mathcal E[x(0)]-\mathcal E[x(s)]\le \frac12\int_0^s |\partial\mathcal E|^2(x(r))\,d\mathcal L^1(r)+\frac12\int_0^s |x'|^2(r)\,d\mathcal L^1(r). \end{align*} Therefore \begin{align*} \mathcal E[x(0)]-\frac12\int_0^s |x'|^2(r)\,d\mathcal L^1(r)-\frac12\int_0^s |\partial\mathcal E|^2(x(r))\,d\mathcal L^1(r)\le \mathcal E[x(s)]. \end{align*} Combining this with the previous upper bound gives \begin{align*} \limsup_{k\to\infty}\mathcal E_k[\bar x_k(s)]\le \mathcal E[x(s)]. \end{align*} Together with the Gamma-liminf inequality \begin{align*} \mathcal E[x(s)]\le\liminf_{k\to\infty}\mathcal E_k[\bar x_k(s)], \end{align*} we conclude that \begin{align*} \mathcal E_k[\bar x_k(s)]\to\mathcal E[x(s)]. \end{align*} [/step] [step:Pass to the limit in the discrete energy-dissipation inequality] Fix $0\le s\le t\le T$. The discrete energy-dissipation inequality gives \begin{align*} \mathcal E_k[\bar x_k(t)]+\frac12\int_s^t a_k^2(r)\,d\mathcal L^1(r)+\frac12\int_s^t g_k^2(r)\,d\mathcal L^1(r)\le \mathcal E_k[\bar x_k(s)]+\varepsilon_k(T). \end{align*} Each of the three terms on the left is bounded from below: the energy term is bounded below by $M$, and the two integral terms are non-negative. Hence the superadditivity of $\liminf$ for finitely many sequences bounded from below gives \begin{align*} \liminf_{k\to\infty}\left(\mathcal E_k[\bar x_k(t)]+\frac12\int_s^t a_k^2(r)\,d\mathcal L^1(r)+\frac12\int_s^t g_k^2(r)\,d\mathcal L^1(r)\right) \end{align*} bounded below by \begin{align*} \liminf_{k\to\infty}\mathcal E_k[\bar x_k(t)]+\frac12\liminf_{k\to\infty}\int_s^t a_k^2(r)\,d\mathcal L^1(r)+\frac12\liminf_{k\to\infty}\int_s^t g_k^2(r)\,d\mathcal L^1(r). \end{align*} Combining this with the endpoint energy lower bound, the metric derivative lower bound, and the slope lower bound yields \begin{align*} \mathcal E[x(t)]+\frac12\int_s^t |x'|^2(r)\,d\mathcal L^1(r)+\frac12\int_s^t |\partial\mathcal E|^2(x(r))\,d\mathcal L^1(r)\le \liminf_{k\to\infty}\mathcal E_k[\bar x_k(s)]. \end{align*} By the endpoint energy identification from the previous step, \begin{align*} \liminf_{k\to\infty}\mathcal E_k[\bar x_k(s)]=\mathcal E[x(s)]. \end{align*} Therefore \begin{align*} \mathcal E[x(t)]+\frac12\int_s^t |x'|^2(r)\,d\mathcal L^1(r)+\frac12\int_s^t |\partial\mathcal E|^2(x(r))\,d\mathcal L^1(r)\le \mathcal E[x(s)]. \end{align*} Since $T>0$ was arbitrary, this holds for every $0\le s\le t<\infty$. Thus $x$ is a curve of maximal slope for $\mathcal E$ with respect to $|\partial\mathcal E|$, and the proof is complete. [/step]