So-called "formal" operations--like "formal differentiation", "formal integration", etc.--have always made me a bit uneasy, because it seems to be used sometimes as a snake-oil solution for dealing with convergence issues, and I've never seen a rigorous explanation of when formal results can be translated to non-formal situations (e.g. algebras of operators over $\mathbb{R}$ or $\mathbb{C}$). I'll give an example below of what I mean, but let me first ask my main question:
Is there some theorem that clarifies when exactly a formal formula can be applied in a non-formal way?
Here's an example: In Lang's book "Real and Functional Analysis" (pg. 401), he wants to evaluate the sum $$S(n) = \frac{1}{n} \sum_{k=1}^n \frac{1}{v-\alpha^k r}$$ where $n\in \mathbb{N}$, $r\in\mathbb{R}$, $\alpha$ is a primitive n-th root of unity, and $v$ is an element of a Banach algebra. To evaluate this, he looks at the formal polynomial $p(t):= t^n - r^n = \prod_{k=1}^n (t-\alpha^k r)$ and takes a formal log derivative to get $\frac{nt^{n-1}}{t^n - r^n} = \sum_{k=1}^n \frac{1}{t-\alpha^k r}$. Then rearranging and plugging in $t=v$ you find $$S(n) = \frac{1}{v-r(r/v)^{n-1}}$$
Now I can justify this to myself by saying that the key relationship $\frac{nt^{n-1}}{t^n - r^n} = \sum_{k=1}^n \frac{1}{t-\alpha^k r}$ can be rearranged into a simple identity equating two representations of a polynomial, which applies equally well to $v$ as to $t$. And that's how these "formal" arguments usually go--a posteriori I can usually justify the conclusion, but it seems really weird to me that we have to enter this netherworld of formal polynomials to justify operations that are "illegal" in the space we actually care about (in the above example, differentiation "with respect to $v$" is not defined in the Banach algebra).
Moreover, it can't always be true that any formal formula can be applied to something like a Banach algebra. For example, implicit in the above example is the fact that the Banach subalgebra generated by $v$ is commutative; if we were trying to apply a multivariate formal formula to two non-commuting elements, it seems we could run into trouble quickly.
So what is a general way of characterizing and understanding the application of formal results to non-formal situations?
The short answer is "juggling homomorphisms." This is more of an art than a science and so I'll explain Lang's example rather than trying to give a general discussion.
The identity
$$\frac{nt^{n-1}}{t^n - r^n} = \sum_{k=1}^n \frac{1}{t - \alpha^k r}$$
lives somewhere. Where does it live? An easy answer is that it lives in the field $\mathbb{C}(t)$ of rational functions over $\mathbb{C}$. But what this field has to do with Banach algebras is unclear. A more interesting answer is that it lives in a subring of this field, namely the localization $\mathbb{C}[t][(t^n - r^n)^{-1}]$ of $\mathbb{C}[t]$ where we invert $t^n - r^n$.
The significance of isolating this ring is that we can apply a "rational functional calculus": rational functions in this ring, which have the form $\frac{f(t)}{(t^n - r^n)^k}$ where $f(t)$ is a polynomial, can be applied to any element $a \in A$ of any $\mathbb{C}$-algebra with the property that $a^n - r^n$ is invertible in $A$. Any such $a$ defines a $\mathbb{C}$-algebra homomorphism
$$\varphi_a : \mathbb{C}[t][(t^n - r^n)^{-1}] \to A$$
which is fully specified by the fact that it sends $t$ to $a$.
In turn, the significance of making this homomorphism explicit is that the formal log derivative is a fully rigorously defined operation on $\mathbb{C}(t)$, whose properties can be fully rigorously proven in this setting. These properties can be used to prove identities which can then be transported via the homomorphism $\varphi_a$ to $A$, even though the proofs don't themselves go through in $A$.
There are more interesting examples where instead of polynomials or rational functions we work with power series, which requires juggling a somewhat more complicated web of homomorphisms. The key point is that any identity between two formal power series with nonzero radius of convergence, established e.g. using formal integration and differentiation or whatever else, must in fact be an identity of holomorphic functions inside the domain of convergence, and then one can apply e.g. holomorphic functional calculus to get non-formal results inside Banach algebras.
Yes, so you only apply such formulas to commuting elements.