Consider the setting:
Let $\Omega \subset \mathbb R^n$, open and bounded with Lipschitz boundary
The Dirichlet integral:
$$I(u)=\int_{\Omega}|\nabla u(x)|^2 dx\tag {5.3}$$
and the class of functions
$\Phi= \{ u \in W^{1,p}(\Omega) : u-g \in W^{1,p}_0(\Omega) \}$ with $g \in W^{1,p}(\Omega)$ given.
In the proof of theorem 5.5 below corollary 5.3 is used. I AM NOT SURE IF $X$ from the corollary is $\Phi$ in the proof Or the whole space $W^{1,2}$. Step 1 (proof of coercivity seems to imply that it is $\Phi$ since they take a sequence in Phi and end up proving that the weak subsequence is also in Phi). What do you think?
Why do they take a sequence in the whole space $W^{1,2}$ in step 2 (proof of lower semicontinuity) instead of in $\Phi$ (as instead is done in the proof of coercivity)? Maybe the proof of lower semicontinuity for the whole space, implies it holds also for the subset? Why yes or why not? (notice that in step 1 for sure this can't be true, there the last step was to prove that the weak subsequence was in the subset $\Phi$)
You can see below the whole proof .
**Whole proof **
Quoted theorems:
In Rindler's Calculus of variations:










After answering your previous post, I've thought about this a bit more. This answer might be longer than necessary, but it's because I think the confusion lies more in the philosophy of writing math than in the rigor of the arguments.
You could conceivably define coercivity and weak lower semi-continuity for any kind of space $X$. However, that definition might not be very useful when trying to prove theorems if the hypotheses on $X$ are too weak. So, one can restrict $X$ to be a reflexive Banach space and easily get the existence of unique minimizers. Then, people like Rindler come along and manage to weaken the hypotheses needed on $X$, and still have the existence of a unique minimizer.
The original author you're quoting defined coercivity for a certain type of space $X$, because they thought it would be enough for the purposes of their text. That definition may or may not apply to $\Phi$ (which isn't a Banach space for example), but that doesn't really matter all that much for the proof of Theorem $5.5$.
The goal of step 1 is to show that a minimizing sequence in $\Phi$ has a subsequence whose limit is also in $\Phi$. Whether the coercivity is proved over $\Phi$ or $W^{1,2}(\Omega)$ doesn't really change the arguments. If it's over $\Phi$, then great, you directly get the existence of a subsequence whose limit is in $\Phi$. If the coercivity is over $W^{1,2}(\Omega)$, then since $\Phi$ is closed and the sequence you're interested in is in $\Phi$, the subsequence's limit is still gonna be in $\Phi$ anyway.
With step 2, the aim is to show that the limit $u$ of our subsequence minimizes $I$. The author does so by showing that $I(u)$ is at least smaller than the limit of $I(u_k)$ can ever be, which relates to the definition of weak lower semi-continuity. Again, whether this is done over $\Phi$ or $W^{1,2}(\Omega)$ doesn't change anything, since both spaces use the same weak topology, and $(u_k)$ was already shown to weakly converge to $u\in\Phi$.
Notice that the author didn't prove in a separate lemma that $I$ is coercive and weakly lower semi-continuous, and then cited an opaque theorem (e.g. Rindler's Theorem 2.3) to conclude it has a unique minimizer. They instead decided to go through the motions of proving the whole thing using just the base hypotheses, and split the proof in multiple steps so that the reader could get a sense of how the machinery works :
and boom, you've shown that a minimizer exists. Now, next time readers encounter a similar problem but with a different $I$ and/or $\Phi$ that don't satisfy the usual theorems' hypotheses, they can try and reuse those arguments to prove it themselves.
So that's why I don't think it matters whether $X$ is $\Phi$ or $W^{1,2}(\Omega)$. Not only is the result the same, the point isn't really to show that $I$ strictly adheres to those definitions, and therefore we have a minimizer. I think it's moreso about showing the general thought process behind proving such a thing in the first place.