Quantile Regression proof I'm interested in understanding the formal proof of why Quantile Regression works. That is, show me in which conditions the pinball/quantile loss provides asymptotic consistent estimations of the conditional quantiles and prove it to me, please.

You don't say what you already know about this and what you want to know, so I'm making some guesses here.  Also, to the best of my knowledge, it isn't known precisely when the estimator is and isn't consistent, so you're just getting sufficient conditions.
First, minimising the pinball loss (a name I don't like, but we're stuck with it now) estimates sample quantiles for a single sample.  To see this, differentiate it. The loss is
$$\sum_i \alpha |x_i-q|\{x_i\geq q\}+(1-\alpha)|x_i-q|\{x_i\leq q\}$$
where $q$ is the estimate. The derivative is $\alpha$ times the number of points above $q$ minus $(1-\alpha)$ times the number of points less than $q$, which crosses zero  at the $\alpha$ quantile.  (Whether it's exactly zero anywhere is slightly complicated, but doesn't matter here)
Since the pinball loss is convex in $q$, if the loss converges pointwise in $q$ it converges uniformly on compact neighbourhoods of the minimum, and the minimiser converges if there's a unique population minimum. This implies the sample quantile is consistent if the data distribution has a non-zero density at the quantile (which is what gives a unique population minimum).  It's also consistent if there is non-zero point mass at the quantile.  It's not consistent if the quantile is the middle of a gap in the distribution.
Moving on to regression, if you want a quantile regression line $x\beta$ to be consistent for all the conditional $\alpha$ quantiles of $y|x$, it is obviously necessary that the conditional quantiles all lie on a line (just as least-squares regression can only be consistent for the conditional means if the conditional means are linear in $x$).  It isn't necessary that all conditional quantiles of $y$ are linear in $x$, just the one you're estimating. However, it's hard for me to think of a setting where you might reasonably know that just the one quantile that you happen to want to estimate is linear, except perhaps if it's the median.  As with least-squares, you might be interested in weaker notions of consistency; if so, you should pick one and ask a question about it.
Suppose, then, that the true $\alpha$ conditional quantiles of $y|x$ lie on a line $x\beta$.  In the population, the expected pinball loss is minimised by that line, because that's what quantiles are.  To get consistency of $\hat\beta$ for $\beta$, we need conditions that will give a law of large numbers for each fixed $\beta$, plus convexity.  One set that works is from here, where the statement and proof are given just for the median. Translating, they say:

*

*$(x,y)$ are iid

*The $x$s have bounded second moment

*There really is a straight line through the conditional quantiles.

*There's a conditional density for $y|x$ with $E[f(q|x)xx^T]>0$ at the conditional quantile

The first condition is weaker than it looks: it says the pairs $(x,y)$ are iid, so it doesn't rule out, say, heteroskedasticity.  The first two conditions are there to ensure a law of large numbers and so could be weakened to allow various sorts of dependence and weaker moment assumptions.  The last condition is like the condition that the density is positive at the median.  The proof (at the link) argues that the loss (scaled by $1/n$) is a convex function of $\beta$ and so pointwise convergence of the loss gives convergence of the estimator to the unique population minimiser, which is the true $\beta$.
