Is the day when these "proofs" are rendered in a natural language coming soon?...

@David Looking for a proof of the primitive element theorem lead me to your answer. You observe that the Bezout resultant is a non-zero polynomial in t, and conclude that it is not the zero polynomial function (of t), which is not always the case. Is it possible to clean the argument?

@Neyman identified a problem with my argument.

@Pietro, Do you see how $sum_i r_i m_i$ is an element of $<r_1,\dots,r_d>_{C^\infty(X)} \otimes_{C^\infty(X)} C^\infty(X\times Y)$? I am working in "coordinates", where the abstract tensor product is made concrete as $<r_1,\dots,r_d>_{C^\infty(X\times Y)}$, and in these coordiantes, the zero function is the zero element. I hope that helps.

@Yemon, my gut feeling is that $C^\infty({\bf R})\otimes_{\bf R} C^\infty({\bf R})$ is not $C^\infty({\bf R^2})$. I will think of a proof. As per my answer, my first step was to verify that $<r_1,\dots,r_d>_{C^\infty(X)} \otimes_{C^\infty(X)} C^\infty(X\times Y) = <r_1,\dots,r_d>_{C^\infty(X\times Y)}$ by checking that any $C^\infty(X)$ bilinear map factors, etc (which is easy), and then I realized I was extending scalars, so I dropped the original argument and appealed to extending scalars.

When $f=0$, $\{X_i\}_i$ is a random drift, and it does not converge. Usually, in iterative methods, the learning rate $\eta$ is assumed to decrease. To second @Mateusz comment, I also doubt the sequence can converge with fixed $\eta$ in general.

'@Iosif I see. You are right, sir

'@Iosif, $E(\eta) \le E(E(\xi| \eta) ) = E(\xi) \le E( E(\eta|\xi)) = E(\eta) $, therefore the inequalities are equalities. Then $E(\xi|\eta) - \eta$ is a non-negative function whose integral is 0, hence $E(\xi|\eta) = \eta$ a.e.; likewise $ E(\eta|\xi)) - \xi$ is a non-negative function whose integral is 0, so $ E(\eta|\xi)) = \xi$ a.e.

As @Iosif mentions, the argument applies with any $g$. One can take $g(x) = x$.

It may be negative. The logarithm of such an expression (or any number) is positive if and only if the expression is greater than or equal to 1.