[proofplan] The proof is obtained by pulling the weak [bilinear form](/page/Bilinear%20Form) on $U$ through the diffeomorphism $\Phi$. The global Lipschitz bounds on $\Phi$ and $\Psi$ justify the Sobolev composition and chain-rule steps, while the [Change of Variables (general)](/theorems/22) contributes the Jacobian factor $|\det J\Psi|$. The ellipticity constants of the transformed matrix follow by applying the ellipticity of $A$ to $J\Phi_{\Psi(y)}^\top\xi$ and using the bounds on $J\Psi$, $J\Phi$, and $|\det J\Psi|$. [/proofplan] [step:Pull the gradients through the diffeomorphism] Define the quantitative bounds \begin{align*} M_\Phi := \operatorname*{ess\,sup}_{x \in U}\|J\Phi_x\|_{\mathrm{op}}. \end{align*} \begin{align*} M_\Psi := \operatorname*{ess\,sup}_{y \in V}\|J\Psi_y\|_{\mathrm{op}}. \end{align*} \begin{align*} M_J := \operatorname*{ess\,sup}_{y \in V}|\det J\Psi_y|. \end{align*} Let $m_J>0$ be a lower bound for $|\det J\Psi_y|$ for $\mathcal L^n$-a.e. $y\in V$. By hypothesis, $\Phi$ and $\Psi$ are globally Lipschitz inverse $C^1$ diffeomorphisms. Together with the two-sided bounds on $|\det J\Psi|$, this verifies the hypotheses of the Sobolev chain rule and Sobolev composition theorem for bi-Lipschitz $C^1$ changes of variables; the underlying measure transformation is the [Change of Variables (general)](/theorems/22). Therefore these results apply to the composition maps \begin{align*} C_\Psi:H^1(U) \to H^1(V), \quad C_\Psi(w)=w\circ \Psi. \end{align*} and \begin{align*} C_\Phi:H^1(V) \to H^1(U), \quad C_\Phi(z)=z\circ \Phi. \end{align*} Thus $v=C_\Psi(u)\in H^1(V)$, $\psi=C_\Psi(\varphi)\in H^1(V)$, and $u=v\circ \Phi$, $\varphi=\psi\circ \Phi$ as Sobolev functions on $U$. The chain rule gives, for $\mathcal{L}^n$-a.e. $x \in U$, \begin{align*} \nabla u(x)=J\Phi_x^\top \nabla v(\Phi(x)). \end{align*} Likewise, \begin{align*} \nabla \varphi(x)=J\Phi_x^\top \nabla \psi(\Phi(x)). \end{align*} It remains to justify the zero boundary condition for $\psi$. Choose a sequence $(\varphi_k)_{k\in\mathbb N}$ in $C_c^\infty(U)$ with $\varphi_k\to\varphi$ in $H^1(U)$, which is possible by the definition of $H^1_0(U)$. The boundedness of $C_\Psi:H^1(U)\to H^1(V)$ gives $\varphi_k\circ\Psi\to\psi$ in $H^1(V)$. For each $k$, the support of $\varphi_k\circ\Psi$ is contained in $\Phi(\operatorname{supp}\varphi_k)$, a compact subset of $V$, and $\varphi_k\circ\Psi\in C_c^1(V)$. By the [Local Approximation Theorem](/theorems/56), $C_c^\infty(V)$ is dense in $C_c^1(V)$ in the $H^1(V)$ norm after mollifying inside a compact subset of $V$. Hence each $\varphi_k\circ\Psi$ lies in the $H^1(V)$-closure of $C_c^\infty(V)$. Therefore $\psi\in H^1_0(V)$. [guided] We first record the constants that will be used later in the ellipticity estimates. Define \begin{align*} M_\Phi := \operatorname*{ess\,sup}_{x \in U}\|J\Phi_x\|_{\mathrm{op}}. \end{align*} \begin{align*} M_\Psi := \operatorname*{ess\,sup}_{y \in V}\|J\Psi_y\|_{\mathrm{op}}. \end{align*} \begin{align*} M_J := \operatorname*{ess\,sup}_{y \in V}|\det J\Psi_y|. \end{align*} Let $m_J>0$ satisfy $|\det J\Psi_y|\geq m_J$ for $\mathcal L^n$-a.e. $y\in V$. The global Lipschitz assumptions on $\Phi$ and $\Psi$ provide the bi-Lipschitz control needed for Sobolev composition. The two-sided bounds on $|\det J\Psi|$ give equivalence of [Lebesgue measure](/page/Lebesgue%20Measure) under [Change of Variables (general)](/theorems/22). These are the hypotheses needed for the Sobolev composition theorem and the Sobolev chain rule under bi-Lipschitz $C^1$ changes of variables. Apply these results to the composition maps \begin{align*} C_\Psi:H^1(U) \to H^1(V), \quad C_\Psi(w)=w\circ \Psi. \end{align*} and \begin{align*} C_\Phi:H^1(V) \to H^1(U), \quad C_\Phi(z)=z\circ \Phi. \end{align*} The theorem's assumptions verify the required bounded derivative, bounded inverse derivative, and measure-comparability hypotheses, so $C_\Psi$ and $C_\Phi$ are bounded maps on $H^1$. Hence $v=u\circ\Psi\in H^1(V)$ and $\psi=\varphi\circ\Psi\in H^1(V)$. Also $u=v\circ\Phi$ and $\varphi=\psi\circ\Phi$ as Sobolev functions on $U$. The chain rule now applies to $u=v\circ\Phi$. At $\mathcal L^n$-a.e. point $x\in U$, it gives \begin{align*} \nabla u(x)=J\Phi_x^\top \nabla v(\Phi(x)). \end{align*} Applying the same chain rule to $\varphi=\psi\circ\Phi$ gives \begin{align*} \nabla \varphi(x)=J\Phi_x^\top \nabla \psi(\Phi(x)). \end{align*} We still have to prove that $\psi$ has zero trace on $V$; this is not merely a pointwise boundary assertion. By definition of $H^1_0(U)$, there is a sequence $(\varphi_k)_{k\in\mathbb N}$ in $C_c^\infty(U)$ such that $\varphi_k\to\varphi$ in $H^1(U)$. Since $C_\Psi:H^1(U)\to H^1(V)$ is bounded, we have \begin{align*} \varphi_k\circ\Psi \to \varphi\circ\Psi=\psi \quad \text{in } H^1(V). \end{align*} For each $k$, the set $\operatorname{supp}\varphi_k$ is compact in $U$. Because $\Phi:U\to V$ is a homeomorphism, $\Phi(\operatorname{supp}\varphi_k)$ is compact in $V$, and \begin{align*} \operatorname{supp}(\varphi_k\circ\Psi)\subset \Phi(\operatorname{supp}\varphi_k). \end{align*} Thus $\varphi_k\circ\Psi$ has compact support in $V$. Since $\Psi$ is $C^1$, the composition $\varphi_k\circ\Psi$ belongs to $C_c^1(V)$. Finally, the [Local Approximation Theorem](/theorems/56) approximates compactly supported $C^1$ functions in the $H^1(V)$ norm by functions in $C_c^\infty(V)$, by mollifying inside a compact subset of $V$. Therefore every $\varphi_k\circ\Psi$ belongs to the $H^1(V)$-closure of $C_c^\infty(V)$, and the $H^1(V)$ limit $\psi$ also belongs to that closure. This proves $\psi\in H^1_0(V)$. [/guided] [/step] [step:Change variables in the weak bilinear form] Using the gradient identities from the previous step, we obtain \begin{align*} \int_U A(x)\nabla u(x)\cdot \nabla \varphi(x)\, d\mathcal{L}^n(x) = \int_U A(x)J\Phi_x^\top\nabla v(\Phi(x))\cdot J\Phi_x^\top\nabla \psi(\Phi(x))\, d\mathcal{L}^n(x). \end{align*} Before changing variables, note that the transformed integrand is integrable. Indeed, the pointwise bound $|A(x)\zeta|\leq \Lambda |\zeta|$, the estimate $\|J\Phi_x\|_{\mathrm{op}}\leq M_\Phi$, and Cauchy-Schwarz give \begin{align*} |A(x)J\Phi_x^\top\nabla v(\Phi(x))\cdot J\Phi_x^\top\nabla \psi(\Phi(x))| \leq \Lambda M_\Phi^2 |\nabla v(\Phi(x))| |\nabla \psi(\Phi(x))|. \end{align*} After composition with $\Phi$ and using $|\det J\Psi|\leq M_J$, the right-hand side is integrable on $V$ because $\nabla v,\nabla\psi\in L^2(V;\mathbb R^n)$. Set $y=\Phi(x)$, so $x=\Psi(y)$. The change-of-variables formula gives \begin{align*} d\mathcal{L}^n(x)=|\det J\Psi_y|\, d\mathcal{L}^n(y). \end{align*} Therefore \begin{align*} \int_U A(x)\nabla u(x)\cdot \nabla \varphi(x)\, d\mathcal{L}^n(x) = \int_V |\det J\Psi_y|\, A(\Psi(y))J\Phi_{\Psi(y)}^\top\nabla v(y)\cdot J\Phi_{\Psi(y)}^\top\nabla \psi(y)\, d\mathcal{L}^n(y). \end{align*} By the definition of matrix transpose and the Euclidean dot product, the integrand on the right is \begin{align*} \widetilde{A}(y)\nabla v(y)\cdot \nabla \psi(y). \end{align*} Thus \begin{align*} \int_U A(x)\nabla u(x)\cdot \nabla \varphi(x)\, d\mathcal{L}^n(x) = \int_V \widetilde{A}(y)\nabla v(y)\cdot \nabla \psi(y)\, d\mathcal{L}^n(y). \end{align*} [guided] The weak form changes by substituting the gradient identities obtained in the previous step. For $\mathcal L^n$-a.e. $x\in U$, those identities are \begin{align*} \nabla u(x)=J\Phi_x^\top \nabla v(\Phi(x)). \end{align*} and \begin{align*} \nabla \varphi(x)=J\Phi_x^\top \nabla \psi(\Phi(x)). \end{align*} Substituting these into the bilinear form gives \begin{align*} \int_U A(x)\nabla u(x)\cdot \nabla \varphi(x)\, d\mathcal{L}^n(x) = \int_U A(x)J\Phi_x^\top\nabla v(\Phi(x))\cdot J\Phi_x^\top\nabla \psi(\Phi(x))\, d\mathcal{L}^n(x). \end{align*} The integrand is integrable because $|A(x)\zeta|\leq \Lambda |\zeta|$, $\|J\Phi_x\|_{\mathrm{op}}\leq M_\Phi$, and the [Cauchy-Schwarz inequality](/theorems/432) give \begin{align*} |A(x)J\Phi_x^\top\nabla v(\Phi(x))\cdot J\Phi_x^\top\nabla \psi(\Phi(x))| \leq \Lambda M_\Phi^2 |\nabla v(\Phi(x))| |\nabla \psi(\Phi(x))|. \end{align*} After the substitution $y=\Phi(x)$, so $x=\Psi(y)$, the [Change of Variables (general)](/theorems/22) applies because $\Phi$ is a $C^1$ diffeomorphism and $|\det J\Psi|$ is bounded above. The measure transforms as \begin{align*} d\mathcal{L}^n(x)=|\det J\Psi_y|\, d\mathcal{L}^n(y). \end{align*} Hence \begin{align*} \int_U A(x)\nabla u(x)\cdot \nabla \varphi(x)\, d\mathcal{L}^n(x) = \int_V |\det J\Psi_y|\, A(\Psi(y))J\Phi_{\Psi(y)}^\top\nabla v(y)\cdot J\Phi_{\Psi(y)}^\top\nabla \psi(y)\, d\mathcal{L}^n(y). \end{align*} By the definition of transpose for the Euclidean dot product, this integrand is exactly $\widetilde{A}(y)\nabla v(y)\cdot \nabla \psi(y)$. Therefore \begin{align*} \int_U A(x)\nabla u(x)\cdot \nabla \varphi(x)\, d\mathcal{L}^n(x) = \int_V \widetilde{A}(y)\nabla v(y)\cdot \nabla \psi(y)\, d\mathcal{L}^n(y). \end{align*} [/guided] [/step] [step:Prove the transformed lower ellipticity bound] Fix $y \in V$ outside the null set on which the ellipticity assumptions for $A(\Psi(y))$ may fail, and fix $\xi \in \mathbb{R}^n$. Define $\eta \in \mathbb{R}^n$ by \begin{align*} \eta := J\Phi_{\Psi(y)}^\top \xi. \end{align*} Then \begin{align*} \xi \cdot \widetilde{A}(y)\xi = |\det J\Psi_y|\, \eta \cdot A(\Psi(y))\eta. \end{align*} Using the ellipticity of $A$ and the lower Jacobian bound, \begin{align*} \xi \cdot \widetilde{A}(y)\xi \geq m_J\theta |\eta|^2. \end{align*} Since $J\Psi_y$ is the inverse of $J\Phi_{\Psi(y)}$, the inverse of $J\Phi_{\Psi(y)}^\top$ is $J\Psi_y^\top$. Hence \begin{align*} |\xi| = |J\Psi_y^\top \eta| \leq \|J\Psi_y\|_{\mathrm{op}}|\eta| \leq M_\Psi |\eta|. \end{align*} Therefore $|\eta| \geq M_\Psi^{-1}|\xi|$, and consequently \begin{align*} \xi \cdot \widetilde{A}(y)\xi \geq \frac{m_J\theta}{M_\Psi^2}|\xi|^2. \end{align*} [/step] [step:Prove the transformed upper bound] Fix $y \in V$ outside the same null set and fix $\xi \in \mathbb{R}^n$. Using the definition of $\widetilde{A}$, the operator norm inequality, the upper bound for $A$, and the bounds on $J\Phi$ and $|\det J\Psi|$, we get \begin{align*} |\widetilde{A}(y)\xi| \leq |\det J\Psi_y|\, \|J\Phi_{\Psi(y)}\|_{\mathrm{op}}\, |A(\Psi(y))J\Phi_{\Psi(y)}^\top \xi|. \end{align*} Since $|A(\Psi(y))\zeta| \leq \Lambda |\zeta|$ for every $\zeta \in \mathbb{R}^n$, \begin{align*} |\widetilde{A}(y)\xi| \leq M_J M_\Phi \Lambda |J\Phi_{\Psi(y)}^\top \xi|. \end{align*} Finally, $|J\Phi_{\Psi(y)}^\top \xi| \leq M_\Phi |\xi|$, so \begin{align*} |\widetilde{A}(y)\xi| \leq M_J M_\Phi^2\Lambda |\xi|. \end{align*} [/step] [step:Conclude that the transformed operator has the same divergence form] The equality of bilinear forms shows that the weak divergence-form expression on $U$ is carried by the coordinate change $\Phi$ to the weak divergence-form expression on $V$ with coefficient matrix $\widetilde{A}$. The preceding two steps show that $\widetilde{A}$ is uniformly elliptic with lower ellipticity constant $m_J\theta/M_\Psi^2$ and upper bound $M_JM_\Phi^2\Lambda$. These constants depend only on $\theta$, $\Lambda$, and the stated quantitative bounds for $\Phi$ and $\Psi$, which proves the theorem. [/step]