[proofplan] Fix a comparison measure $\nu\in D(\mathcal E)$. Local absolute continuity of the curve $\rho$ first implies local absolute continuity of the squared distance to $\nu$. At almost every time where the continuity equation, finite energy, and the squared-distance derivative formula hold, choose an optimal plan from $\rho_t$ to $\nu$. The derivative formula identifies the time derivative of \begin{align*} \frac{1}{2}W_2(\rho_t,\nu)^2 \end{align*} with the same optimal-transport pairing that appears in the strong Wasserstein subdifferential inequality. Substituting that identity into the subdifferential inequality gives the evolution variational inequality. [/proofplan]

[step:Show that the squared distance to the comparison measure is locally absolutely continuous]Fix $\nu\in D(\mathcal E)$. Let $[a,b]\subset(0,\infty)$ be a compact interval, and let $\mathcal B([a,b])$ denote the Borel $\sigma$-algebra of $[a,b]$. Since the map $\rho:[a,b]\to(\mathcal P_2(\mathbb R^n),W_2)$ is absolutely continuous, there exists a function \begin{align*} g:[a,b]\to[0,\infty] \end{align*} with $g\in L^1([a,b],\mathcal B([a,b]),\mathcal L^1)$ such that, for every $a\le s\le t\le b$, \begin{align*} W_2(\rho_s,\rho_t)\le \int_s^t g(r)\,d\mathcal L^1(r). \end{align*} By the triangle inequality in the metric space $(\mathcal P_2(\mathbb R^n),W_2)$, \begin{align*} |W_2(\rho_t,\nu)-W_2(\rho_s,\nu)|\le W_2(\rho_s,\rho_t)\le \int_s^t g(r)\,d\mathcal L^1(r). \end{align*} Thus the map \begin{align*} h_\nu:[a,b]\to[0,\infty),\qquad t\mapsto W_2(\rho_t,\nu) \end{align*} is absolutely continuous. Because $h_\nu$ is continuous on the compact interval $[a,b]$, define \begin{align*} M_{a,b,\nu}:=\sup_{r\in[a,b]}h_\nu(r)<\infty. \end{align*} For every $s,t\in[a,b]$, \begin{align*} |h_\nu(t)^2-h_\nu(s)^2|=|h_\nu(t)-h_\nu(s)|\,|h_\nu(t)+h_\nu(s)|\le 2M_{a,b,\nu}|h_\nu(t)-h_\nu(s)|. \end{align*} Hence \begin{align*} f_\nu:[a,b]\to[0,\infty),\qquad t\mapsto W_2(\rho_t,\nu)^2 \end{align*} is absolutely continuous. Since $[a,b]\subset(0,\infty)$ was arbitrary, $f_\nu$ is locally absolutely continuous on $(0,\infty)$.[/step]

[guided]We first prove the regularity of the function whose derivative will appear in the EVI. Fix $\nu\in D(\mathcal E)$ and fix a compact interval $[a,b]\subset(0,\infty)$. Let $\mathcal B([a,b])$ denote the Borel $\sigma$-algebra of $[a,b]$. The curve $\rho:[a,b]\to(\mathcal P_2(\mathbb R^n),W_2)$ is absolutely continuous by hypothesis. This means that there is a function \begin{align*} g:[a,b]\to[0,\infty] \end{align*} with $g\in L^1([a,b],\mathcal B([a,b]),\mathcal L^1)$ such that, whenever $a\le s\le t\le b$, \begin{align*} W_2(\rho_s,\rho_t)\le \int_s^t g(r)\,d\mathcal L^1(r). \end{align*} The distance to a fixed point is $1$-Lipschitz in any metric space. Applying the triangle inequality in $(\mathcal P_2(\mathbb R^n),W_2)$ gives \begin{align*} |W_2(\rho_t,\nu)-W_2(\rho_s,\nu)|\le W_2(\rho_s,\rho_t). \end{align*} Combining this with the absolute-continuity estimate for $\rho$ gives \begin{align*} |W_2(\rho_t,\nu)-W_2(\rho_s,\nu)|\le \int_s^t g(r)\,d\mathcal L^1(r). \end{align*} Therefore the map \begin{align*} h_\nu:[a,b]\to[0,\infty),\qquad t\mapsto W_2(\rho_t,\nu) \end{align*} is absolutely continuous. We need the square of this distance, not only the distance itself. Since $h_\nu$ is continuous on the compact interval $[a,b]$, it is bounded there. Define \begin{align*} M_{a,b,\nu}:=\sup_{r\in[a,b]}h_\nu(r). \end{align*} This number is finite. For all $s,t\in[a,b]$, the algebraic identity $A^2-B^2=(A-B)(A+B)$ gives \begin{align*} |h_\nu(t)^2-h_\nu(s)^2|=|h_\nu(t)-h_\nu(s)|\,|h_\nu(t)+h_\nu(s)|. \end{align*} Since both $h_\nu(t)$ and $h_\nu(s)$ are bounded by $M_{a,b,\nu}$, we obtain \begin{align*} |h_\nu(t)^2-h_\nu(s)^2|\le 2M_{a,b,\nu}|h_\nu(t)-h_\nu(s)|. \end{align*} The composition of an absolutely continuous function with a Lipschitz function on the range of that curve is absolutely continuous, and the displayed estimate gives the needed Lipschitz control on the squaring map over the bounded interval $[0,M_{a,b,\nu}]$. Hence \begin{align*} f_\nu:[a,b]\to[0,\infty),\qquad t\mapsto W_2(\rho_t,\nu)^2 \end{align*} is absolutely continuous. Since the compact interval $[a,b]\subset(0,\infty)$ was arbitrary, $f_\nu$ is locally absolutely continuous on $(0,\infty)$.[/guided]

[step:Select full-measure times where the derivative and subdifferential identities are valid]Let $N_\nu\subset(0,\infty)$ be the set of times $t$ for which at least one of the following fails: $\rho_t\in D(\mathcal E)$, $v_t\in L^2(\mathbb R^n,\mathcal B(\mathbb R^n),\rho_t;\mathbb R^n)$, $v_t$ is the tangent velocity of the Wasserstein absolutely continuous curve $\rho$, the derivative $\frac{d}{dt}W_2(\rho_t,\nu)^2$ exists, the strong Wasserstein subdifferential inequality in the theorem statement holds for the fixed comparison measure $\nu$ and every optimal plan $\gamma\in\Gamma_o(\rho_t,\nu)$, or the derivative formula \begin{align*} \frac{1}{2}\frac{d}{dt}W_2(\rho_t,\nu)^2 = \int_{\mathbb R^n\times\mathbb R^n} v_t(x)\cdot(x-y)\,d\gamma_t(x,y) \end{align*} holds for every optimal transport plan $\gamma_t\in\Gamma_o(\rho_t,\nu)$. The local square-integrability of $v$ on compact time intervals, the spacetime distributional continuity equation, and the tangent-velocity assumption make $v$ an admissible minimal velocity field for the locally absolutely continuous Wasserstein curve $\rho$. The first-variation formula for the squared $W_2$ distance along Wasserstein absolutely continuous curves with tangent velocity therefore applies to the pair $(\rho,v)$. Together with the local absolute continuity proved above and the a.e. strong subdifferential hypothesis, this implies that the set $N_\nu$ has $\mathcal L^1$-measure zero. Fix $t\in(0,\infty)\setminus N_\nu$. Since $\rho_t,\nu\in\mathcal P_2(\mathbb R^n)$, there exists at least one optimal transport plan from $\rho_t$ to $\nu$. Choose one and denote it by \begin{align*} \gamma_t\in\Gamma_o(\rho_t,\nu). \end{align*} For this plan, the derivative formula gives \begin{align*} \frac{1}{2}\frac{d}{dt}W_2(\rho_t,\nu)^2 = \int_{\mathbb R^n\times\mathbb R^n} v_t(x)\cdot(x-y)\,d\gamma_t(x,y). \end{align*} Since $v_t(x)\cdot(x-y)=(-v_t(x))\cdot(y-x)$ for every $(x,y)\in\mathbb R^n\times\mathbb R^n$, we have \begin{align*} \frac{1}{2}\frac{d}{dt}W_2(\rho_t,\nu)^2 = \int_{\mathbb R^n\times\mathbb R^n}(-v_t(x))\cdot(y-x)\,d\gamma_t(x,y). \end{align*} Here the first-variation formula for squared $W_2$ distance along Wasserstein absolutely continuous curves with tangent velocity is the external prerequisite; the tangent-velocity and local spacetime $L^2$ hypotheses above are precisely the hypotheses used to apply it.[/step]

[guided]Fix $\nu\in D(\mathcal E)$. We now isolate the times at which all pointwise-in-time identities used in the EVI argument are legitimate. By hypothesis, $\rho_t\in D(\mathcal E)$ for $\mathcal L^1$-a.e. $t>0$, and $v_t\in L^2(\mathbb R^n,\mathcal B(\mathbb R^n),\rho_t;\mathbb R^n)$ for $\mathcal L^1$-a.e. $t>0$. The strengthened statement also gives \begin{align*} \int_a^b\int_{\mathbb R^n}|v_t(x)|^2\,d\rho_t(x)\,d\mathcal L^1(t)<\infty \end{align*} for every compact interval $[a,b]\subset(0,\infty)$, the continuity equation holds in the sense of distributions on spacetime, and $v_t$ is the tangent velocity of $\rho$ for $\mathcal L^1$-a.e. $t>0$. These are exactly the admissibility hypotheses needed to use the first-variation formula for the squared $W_2$ distance along a Wasserstein absolutely continuous curve with tangent velocity. Let $N_\nu\subset(0,\infty)$ be the exceptional set where at least one required property fails: finite energy of $\rho_t$, square-integrability of $v_t$, the tangent-velocity property, existence of the derivative of $t\mapsto W_2(\rho_t,\nu)^2$, validity of the strong subdifferential inequality for the fixed comparison measure $\nu$ and every optimal plan from $\rho_t$ to $\nu$, or validity of the first-variation formula. Since $t\mapsto W_2(\rho_t,\nu)^2$ is locally absolutely continuous, the derivative formula applies to the admissible tangent-velocity pair $(\rho,v)$, and the subdifferential inequality holds for $\mathcal L^1$-a.e. $t>0$ by hypothesis, this exceptional set has $\mathcal L^1$-measure zero. Fix $t\in(0,\infty)\setminus N_\nu$. Because $\rho_t$ and $\nu$ lie in $\mathcal P_2(\mathbb R^n)$, the quadratic optimal transport problem between them admits an optimal plan. Choose one and denote it by \begin{align*} \gamma_t\in\Gamma_o(\rho_t,\nu). \end{align*} The first-variation formula gives \begin{align*} \frac{1}{2}\frac{d}{dt}W_2(\rho_t,\nu)^2 = \int_{\mathbb R^n\times\mathbb R^n} v_t(x)\cdot(x-y)\,d\gamma_t(x,y). \end{align*} Finally, for every $(x,y)\in\mathbb R^n\times\mathbb R^n$, the Euclidean dot product satisfies $v_t(x)\cdot(x-y)=(-v_t(x))\cdot(y-x)$. Substituting this identity inside the integral yields \begin{align*} \frac{1}{2}\frac{d}{dt}W_2(\rho_t,\nu)^2 = \int_{\mathbb R^n\times\mathbb R^n}(-v_t(x))\cdot(y-x)\,d\gamma_t(x,y). \end{align*}[/guided]

[step:Insert the derivative formula into the strong Wasserstein subdifferential inequality]The strong Wasserstein subdifferential hypothesis applies at the fixed time $t\in(0,\infty)\setminus N_\nu$, to the fixed comparison measure $\nu\in D(\mathcal E)$, and to the chosen optimal plan $\gamma_t\in\Gamma_o(\rho_t,\nu)$. Therefore \begin{align*} \mathcal E[\nu]-\mathcal E[\rho_t]\ge \int_{\mathbb R^n\times\mathbb R^n}(-v_t(x))\cdot(y-x)\,d\gamma_t(x,y)+\frac{\lambda}{2}W_2(\rho_t,\nu)^2. \end{align*} Using the identity from the preceding step, this becomes \begin{align*} \mathcal E[\nu]-\mathcal E[\rho_t]\ge \frac{1}{2}\frac{d}{dt}W_2(\rho_t,\nu)^2+\frac{\lambda}{2}W_2(\rho_t,\nu)^2. \end{align*} Rearranging gives \begin{align*} \frac{1}{2}\frac{d}{dt}W_2(\rho_t,\nu)^2+\frac{\lambda}{2}W_2(\rho_t,\nu)^2+\mathcal E[\rho_t]\le \mathcal E[\nu]. \end{align*} This holds for every $t\in(0,\infty)\setminus N_\nu$, and $N_\nu$ has $\mathcal L^1$-measure zero. Hence the asserted evolution variational inequality holds for $\mathcal L^1$-a.e. $t>0$.[/step]

[guided]Fix $t\in(0,\infty)\setminus N_\nu$ and use the optimal plan \begin{align*} \gamma_t\in\Gamma_o(\rho_t,\nu) \end{align*} chosen in the preceding step. At this time the strong Wasserstein subdifferential hypothesis is valid, $\rho_t\in D(\mathcal E)$, and $\nu\in D(\mathcal E)$ by the original choice of comparison measure. Therefore \begin{align*} \mathcal E[\nu]-\mathcal E[\rho_t]\ge \int_{\mathbb R^n\times\mathbb R^n}(-v_t(x))\cdot(y-x)\,d\gamma_t(x,y)+\frac{\lambda}{2}W_2(\rho_t,\nu)^2. \end{align*} The previous step identified the transport pairing in this inequality with the time derivative of the squared distance: \begin{align*} \int_{\mathbb R^n\times\mathbb R^n}(-v_t(x))\cdot(y-x)\,d\gamma_t(x,y) = \frac{1}{2}\frac{d}{dt}W_2(\rho_t,\nu)^2. \end{align*} Substituting this identity gives \begin{align*} \mathcal E[\nu]-\mathcal E[\rho_t]\ge \frac{1}{2}\frac{d}{dt}W_2(\rho_t,\nu)^2+\frac{\lambda}{2}W_2(\rho_t,\nu)^2. \end{align*} Adding $\mathcal E[\rho_t]$ to both sides yields \begin{align*} \frac{1}{2}\frac{d}{dt}W_2(\rho_t,\nu)^2+\frac{\lambda}{2}W_2(\rho_t,\nu)^2+\mathcal E[\rho_t]\le \mathcal E[\nu]. \end{align*} Since the exceptional set $N_\nu$ has $\mathcal L^1$-measure zero, this proves the EVI for $\mathcal L^1$-a.e. $t>0$.[/guided]