Countable (?) dependent choice In some circumstances I've been using a form of choice over the first uncountable ordinal knowing a priori that only a countable number of choices were going to be made (without any a priori upper bound). I would like to know whether I was using the classical dependent choice or something stronger and in case how much stronger.
I think the argument that I have in mind is better explained with an example and the best that I know is a proof of Ekeland's variation principle. 
Such principle establishes the existence of `almost mininizers' of a function on a non-compact, but complete, metric space. Let me give a - somehow suboptimal - formulation of the result:
Theorem Let $(X,d)$ be a complete metric space and $f:X\to[0,+\infty)$ lower semicontinuous (one can assume $f$ to be continuous if he wishes). Let $\epsilon>0$. Then there exists a point $x\in X$ such that $f(x)\leq\inf f+\epsilon$ and satisfying
$$
f(y)\geq f(x)-\epsilon d(x,y)\qquad\forall y\in X.
$$
Thus if we could choose $\epsilon=0$ the theorem would provide the existence of a minimum for $f$, so that the requirement $\epsilon>0$ might be seen as a sort of almost minimization (also known as quasi-minimization in some contexts).
Here is a possible proof of the theorem: Let $\Omega$ be the first uncountable ordinal and let's recursively define a map $\Omega\ni \alpha\to x_\alpha\in X$ as follows. $x_0\in X$ is taken arbitrarily such that $f(x_0)<\inf f+\epsilon$. If  $x_\alpha$ has already been defined, we define $x_{\alpha+1}$ as follows: if $x_{\alpha}$ satisfies the conclusion of the theorem, we put $x_{\alpha+1}:=x_{\alpha}$. Otherwise the set of $y$'s such that 
$$
f(y)< f(x_{\alpha})-\epsilon d(x_{\alpha},y)
$$
is not empty: let $x_{\alpha+1}$ be any of these $y$'s. Thus in particular we have
$$
\epsilon d(x_\alpha,x_{\alpha+1})<f(x_{\alpha})-f(x_{\alpha+1}).\qquad (1)
$$
If $\alpha\in\Omega$ is a limit ordinal we define 
$$
x_\alpha:=\lim_{\beta\uparrow\alpha}x_\beta.
$$
We need to show that this is a good definition, i.e. that the limit exists. Let's examine the case $\alpha=\omega$ at first. Adding up (1) over $\alpha\in\mathbb N$ we see that 
$$
\epsilon\sum_{n\in\mathbb N} d(x_n,x_{n+1})\leq f(x_0)<\infty
$$
and this forces the sequence $(x_n)$ to be Cauchy, so that (since $(X,d)$ is assumed to be complete) $x_\omega$ is well defined. For general limit ordinals $\alpha$ the argument is the same: one has to observe that (1) and transfinite induction show that for $\beta\leq \beta'<\alpha$ it holds
$$
\epsilon d(x_\beta,x_{\beta'})<f(x_{\beta})-f(x_{\beta'})
$$
so that one can conclude that the limit of $x_\beta$ exists arguing as before and, for instance, using the fact that any countable ordinal is the limit of an increasing sequence of smaller ordinals. 
Hence $x_\alpha$ is now defined for every $\alpha<\Omega$. Let us now look at the map $\alpha\to f(x_\alpha)$. By construction this map is non-increasing: this is trivial for successor ordinals, for limit ones we use the (semi)continuity of $f$. But any monotone map from $\Omega$ to $\mathbb R$ must be eventually constant: in our notation this follows by noticing that the open sets $(f(x_{\alpha}),f(x_{\alpha+1}))$ are all disjoint and thus only a countable number of them can be non-empty.
Hence $\alpha\to f(x_\alpha)$ must be eventually constant and in particular for some $\alpha$ we must have $f(x_\alpha)=f(x_{\alpha+1})$. However, by construction this means that $x_\alpha$ satisfies the conclusion of the theorem, because otherwise (1) forces $f(x_{\alpha+1})<f(x_\alpha)$. Thus the proof is achieved.
Notice that albeit the $x_\alpha$'s are defined over all $\Omega$, in fact only a countable number of choices have been made, because the function $\alpha\to f(x_\alpha)$ is eventually constant.
I would like to know:
a) is this argument using the standard axiom of dependent choice, a different form of countable dependent choice or some uncountable version of it?
b) is the `choice axiom' used in the proof compatible with the measurability of all the subsets of the reals?
Perhaps I should mention that Ekeland's proof of the above theorem relies on the standard dependent choice. The idea is that instead of randomly picking $x_{n+1}$, one chooses one which makes a `sufficiently big step', here is Ekeland's proof:
Pick $x_0\in X$ as above and for given $x_n$ define the closed set $S_n\subset X$ as
$$
S_n:=\{y\ : \ f(y)\leq f(x_n)-\epsilon d(x_n,y)\}.
$$
Then pick $x_{n+1}\in S_n$ such that
$$
f(x_n)-f(x_{n+1})\geq\frac12\big(f(x_n)-\inf_{y\in S_n}f(y)\big)\qquad (2)
$$
Then the same arguments previously used ensure that $(x_n)$ is a Cauchy sequence while from the requirement (2) it is easy to see that the limit point fulfills the requirements.
The 'problem' that I have with this argument is that it is `more complicated' (of course this is highly debatable) because it needs the idea of forcing the choice as in (2), rather than simply saying 'if I'm not arrived, I move on'. Beside this particular case, I've found myself using the argument involving ordinals even in situations where I would not know what is the analogue of (2), in particular because there appears to be no function to be almost-minimized. Thus I would like to understand which form of choice I'm using and its relation with other axioms typically related with countable forms of choice.
 A: There has been some recent interest in the reverse mathematics of Ekeland's theorem. At the latest meeting of the Association of Symbolic Logic, Paul Shafer presented some of his work with David Fernández-Duque, Henry Towsner and Keita Yokoyama the reverse analysis of Ekeland's theorem and Caristi's theorem. Hopefully this work will be available soon. Now on the arxiv: 1902.03915.
Meanwhile, I can talk about the proof method described in the question to answer (a) and (b). The proposed proof relies on the principle of $\omega_1$-dependent choice ($\mathsf{DC}_{\omega_1}$), which can be stated as follows:

If $R \subseteq A^{<\omega_1}\times A$ is total then there is a function $x:\omega_1\to A$ such that $R(x{\upharpoonright}\alpha,x(\alpha))$ for all $\alpha<\omega_1$.

($\omega_1$ is the first uncountable ordinal; $A^{<\omega_1}$ denotes the set of all functions $x:\alpha\to A$ where $\alpha$ is a countable ordinal; to say $R$ is total means that for every such $x:\alpha \to A$ there is a $y \in A$ such that $R(x,y)$ holds.)
What is perhaps confusing is that this is a proof by contradiction, so it appears that the full power of $\mathsf{DC}_{\omega_1}$ is not actually used. This is an illusion. Schematically, the proof can be presented as follows which shows more clearly the use of $\mathsf{DC}_{\omega_1}$:


*

*Assume $\mathsf{DC}_{\omega_1}$ and that Ekeland's theorem is false for $X$ and $f:X\to[0,\infty)$.

*Then the relation $R \subseteq X^{<\omega_1}\times X$ is total where $R(x,y)$ holds for $x:\alpha\to X$ and $y \in X$ if:


*

*$\alpha = 0$ and $y$ is arbitrary;

*$\alpha = \beta+1$ and $f(y) < f(x(\beta)) - \varepsilon d(x(\beta),y)$;

*$\alpha$ is a limit ordinal and either $y = \lim_{\beta<\alpha} x(\beta)$, 
or this limit does not exist and $y$ is arbitrary.


*From $\mathsf{DC}_{\omega_1}$ there exists $x:\omega_1\to X$ such that $R(x{\upharpoonright}\alpha,x(\alpha))$ holds for every $\alpha<\omega_1$.

*Note that $\lim_{\beta<\alpha} x(\beta)$ exists for every limit ordinal $\alpha<\omega_1$, so we always have $x(\alpha) = \lim_{\beta<\alpha} x(\beta)$ 

*By the lower semicontinuity of $f$, we then see that $f(x(\beta)) > f(x(\alpha))$ when $\beta < \alpha < \omega_1$. This is impossible since there is no uncountable decreasing sequence of real numbers.

*From this contradiction, we conclude that our hypothesis from step 1 is false: it is not true that $\mathsf{DC}_{\omega_1}$ holds and Ekeland's theorem is false. In other words, $\mathsf{DC}_{\omega_1}$ implies Ekeland's theorem.


This does not mean that Ekeland's theorem requires $\mathsf{DC}_{\omega_1}$, but this argument makes essential use of $\mathsf{DC}_{\omega_1}$. Unfortunately, $\mathsf{DC}_{\omega_1}$ also implies that there is a nonmeasurable set of reals. Indeed, it is trivial to use $\mathsf{DC}_{\omega_1}$ to construct an injection $\omega_1 \to \mathbb{R}$. A celebrated result of Raisonnier says that this implies that there is a nonmeasurable set of reals.
Raisonnier, Jean, A mathematical proof of S. Shelah’s theorem on the measure problem and related results, Isr. J. Math. 48, 48-56 (1984). ZBL0596.03056.
