Edit: Here's a more down-to-earth, and somewhat weakened, but I believe still nontrivial, version of the main theorem.
Prototypical nonconvex spaces are $\ell^p$-spaces for $0<p<1$, say $\ell^p(\mathbb N)$ with norm $||(x_n)_n|| = \sum_n |x_n|^p$. This is in fact a projective object in the category of $p$-Banach spaces. However, it fails to be projective in the larger category of quasi-Banach spaces (by the Aoki--Rolewicz theorem, those are those complete topological vector spaces that admit a $q$-norm, i.e. are a $q$-Banach, for some $0<q\leq 1$), and in fact it has nontrivial self-extensions. However, Dustin Clausen and I proved that the smaller object $\ell^{p'}(\mathbb N)$ for $p'<p$ behaves like a projective object when tested against $p$-Banachs:
Theorem. Let $0<p'<p\leq 1$ and let $V$ be a $p$-Banach. Then, for the Yoneda-Ext groups in quasi-Banach spaces, $$ \mathrm{Ext}^i(\ell^{p'}(\mathbb N),V)=0$$ for all $i>0$.
The Yoneda-Ext group $\mathrm{Ext}^i$ classifies exact sequences with $i+2$ terms $$0\to V\to W_1\to\ldots\to W_i\to \ell^{p'}(\mathbb N)\to 0$$ where all $W_n$ are quasi-Banachs (but possibly only $q$-Banach for $q<p'$), up to a certain notion of equivalence. The case $i=1$ is a theorem of Kalton.
Nonconvexity means that many standard tools break down. The way Dustin Clausen and I overcame this problem here was to use the following simple
Proposition. Let $r=\tfrac 1{10^p}$ and let $C=\tfrac{10}{1-r}$. Then for all $x\in \mathbb R$, one has $$ |x|^p\leq \mathrm{inf}\{\sum_n |x_n| r^n\mid x_n\in \mathbb Z, \sum_n \tfrac{x_n}{10^n} = x\}\leq C|x|^p. $$
See Pavel's answer for a quick proof (for general $\tilde{r}=\tfrac 1{10}$).
What this proposition achieves is that it translates the nonconvex $|x|^p$ into the convex $|x_n|$ for discrete $x_n\in \mathbb Z$, at the various scales $10^{-n}$. Using this proposition, we were able to use convex geometry in a discretized setting to solve our problem.
Main Question: Are there any previous arguments of a similar sort, reducing a continuous nonconvex problem to a discrete convex problem on different scales?
Alternatively, I'd be very interested in a different approach to this theorem. (In the version we prove, we know even less about the nature of the intermediate $W_n$; so I'm not completely sure whether the whole complexity is preserved. However, a sanity check is that also for us, the $i=1$ case is significantly easier than $i>1$, and can be done by a direct attack.)
Below is the long, rambling, original question. I recommend reading the paragraph starting with "Say you want to travel from A to B" to get some intuition for what happens in the proposition.
Three months ago, I wrote the blog post Liquid Tensor Experiment, posing a challenge to verify a certain proof. The computer formalization is proceeding extremely well, I am really impressed by the efforts.
But this question is about the "human" part of that same proof: I think I still don't understand (or am just beginning to understand, with writing this question a key part of this) what is happening in our proof. I can roughly follow the proof line-by-line, but I don't have a real understanding for why it works, or am only slowly getting it. (I realize that this is an awkward thing to say about one's own proof. There's a reason I want a verification...)
Let me state the theorem in question. There are three inputs:
The category of condensed abelian groups --- a version of topological abelian groups, but forming an abelian category --- in which this computation takes place. For an introduction to this, see the blog post. For the kind of "big picture" question I want to ask, it is however not very relevant.
A $p$-Banach space $V$, for some $0<p\leq 1$. Recall that this is a complete normed real vector space $(V,||\cdot||)$ where the norm satisfies the usual triangle inequality, but the scaling behaviour $||ax||=|a|^p ||x||$ for $a\in \mathbb R$, $x\in V$. In particular, for $p<1$, these may be non-locally convex. A prototypical example are $\ell^p$-spaces; say $\ell^p(\mathbb N)$ with norm $||(x_n)_n|| = \sum_n |x_n|^p$.
The space $\mathcal M_p(S)$ of $p$-measures on some profinite set $S$, where again $0<p\leq 1$. If $p=1$, this is the usual space of (signed Radon) measures on $S$, which we equip with the compactly generated weak-$\ast$-topology. In other words, $\mathcal M_1(S)$ is a rising union (with the colimit topology) of compact Hausdorff spaces $\mathcal M_1(S)_{\leq c}$ for $c\in \mathbb R_{\geq 0}$. Here, for finite $S$, one has $\mathcal M_p(S)=\mathbb R[S]$ the free $\mathbb R$-vector space on $S$ with the $\leq c$-subspace given by $\{(x_s)_{s\in S}\mid \sum_{s\in S} |x_s|\leq c\}$, and in general for a profinite $S=\varprojlim_i S_i$, one sets $$\mathcal M_1(S)_{\leq c} = \varprojlim_i \mathcal M_1(S_i)_{\leq c}.$$ For general $p$, one does the very same thing, replacing the $\ell^1$-norm with the $\ell^p$-norm. In other words, for finite sets $S$ we still have $\mathcal M_p(S)=\mathbb R[S]$, but the $\leq c$-subspace is given by $\{(x_s)_s\mid \sum_{s\in S} |x_s|^p\leq c\}$, then for profinite $S=\varprojlim_i S_i$ one takes $$\mathcal M_p(S)_{\leq c} = \varprojlim_i \mathcal M_p(S_i)_{\leq c}$$ and finally $\mathcal M_p(S)$ is the rising union of the $\mathcal M_p(S)_{\leq c}$. Just like one can define a space of signed Radon measures on any compact Hausdorff space $S$, the same is actually also true for the space of $p$-measures on $S$; one way to define it is to write $S=\tilde{S}/R$ as a quotient of a profinite set $S$ by a closed equivalence relation $R$, and then set $\mathcal M_p(S)=\mathcal M_p(\tilde{S})/\mathcal M_p(R)$. I do not really have a good direct definition of it. Also, for $p<1$, any element of $\mathcal M_p(S)$ is actually just a countable sum of Dirac measures, with $p$-summable coefficients; but the topology is more subtle.
Preliminary Question. What is some previous literature on this space of $p$-measures?
Now one can show that if $V$ is any $p$-Banach space, and $f: S\to V$ is any continuous map, then it extends uniquely to a map $\mathcal M_p(S)\to V$ of topological real vector spaces (which reduces to $f$ on Dirac measures). What we originally hoped for, for $p=1$ in fact, is that this uniqueness is true even "in the higher sense"; more precisely:
Is $\mathrm{Ext}^i(\mathcal M_p(S),V)=0$ for $i>0$?
It turns out that this is false: One can show that there are explicit $\mathrm{Ext}^1$-classes, first constructed by Ribe, coming from the entropy function. (I hadn't expected to run into the entropy functional any day soon...) In a first try, we then passed to measures of "bounded entropy", on which these extensions split; but they acquire new extensions of their own, leading to infinite regress. So one needs to replace $\mathcal M_p(S)$ by some space of measures distinctly smaller than $\mathcal M_p(S)$; for example $\mathcal M_{p'}(S)$ for $p'<p$.
This led Clausen and myself to conjecture, and eventually prove, the following theorem (which is the one for which I want a computer verification):
Theorem. If $0<p'<p\leq 1$ and $V$ is a $p$-Banach space, then $\mathrm{Ext}^i(\mathcal M_{p'}(S),V)=0$ for $i>0$.
This theorem is the basis for the "$p$-liquid analytic ring structure" on the reals; I refer you again to the blogpost for some discussion about this.
Basically, the intuition here is that if you have a $p'$-measure $\mu$, then you can split it into $N$ summands that are either Dirac measures, or are of $p'$-norm roughly $\tfrac 1N$ of the $p'$-norm of the original sequence; mapping to $V$, we know where the Dirac measures go, and the other terms have very small image in $V$, as the norm scales differently on $V$. Any such decomposition of $\mu$ can be thought of as a path connecting a given measure to Dirac measures. To see that higher Ext-groups vanish, one needs to see that for any two such paths, there is some homotopy connecting them, also being sufficiently small; and higher homotopies between those.
Unfortunately, this seems to be a bit tricky, as in a nonconvex shape, it is hard to find enough free room to move around: You cannot simply take the average of two maps if you want to keep track of bounds. So roughly, any such decomposition is like some valley in a function you would like to minimize, but now you have to connect different valleys without climbing too high; that's tricky.
The way we (inadvertently -- see the following comments) solved this issue is by passing to a discretization of the problem, where the discretized problem is convex. (Our original motivation for the discretization was in some sense of a purely technical sort, having to do with the nature of the category of condensed abelian groups; this motivation is explained in the blog post. Only recently, when in the formalization process a significant amount of convex geometry has to be formalized, did I realize that we're using convex geometry in a critical way, and that this is a much more profound reason for the discretization.)
More precisely, for some fixed radius $r$ with $0<r<1$, or let's in fact say $\tfrac 1{10}<r<1$, we consider the ring
$$\mathbb Z((T))_r = \{\sum a_n T^n\mid \sum |a_n| r^n<\infty\}$$
of arithmetic Laurent series with a certain convergence condition; in particular such sums converge for $0<|T|<r$. In particular, we can evaluate at $T=\tfrac 1{10}$ and get a surjection
$$\mathbb Z((T))_r\to \mathbb R: \sum a_n T^n\mapsto \sum \frac{a_n}{10^n}$$
in some sense recording decimal expansions of real numbers. The map is surjective, and the kernel is generated by $10T-1$.
Now for finite sets $S$, we can again endow the free module $\mathcal M(S,\mathbb Z((T))_r)=\mathbb Z((T))_r[S]$ with a "norm", by looking at the subspaces
$$\mathcal M(S,\mathbb Z((T))_r)_{\leq c} = \{\sum_{n,s} a_{n,s} T^n [s]\mid \sum_{n,s} |a_{n,s}| r^n\leq c\}.$$
In other words, we use the usual (convex) absolute value on $\mathbb Z$, and set $|T|=r$. This is naturally a (totally disconnected) compact Hausdorff space. Again, for profinite $S$ we can pass to the limit, and then get the space of measures
$$\mathcal M(S,\mathbb Z((T))_r) = \bigcup_c \mathcal M(S,\mathbb Z((T))_r)_{\leq c}$$
for general profinite sets $S$. (Again, one can also build a version for general compact Hausdorff $S$, passing to quotients.)
The key observation is the following (see Theorem 6.9 (2), Proposition 7.2 here):
Proposition. There is a canonical isomorphism $$\mathcal M(S,\mathbb Z((T))_r)/(10T-1)\cong \mathcal M_{p'}(S,\mathbb R),$$ where $0<p'<1$ is chosen so that $r=10^{-p'}$.
(More precisely, a unique functorial one compatible with Dirac measures.)
The key is that the left-hand side is convex but discretized, while the right-hand side is non-convex. To understand what is happening here, let me make an analogy:
Say you want to travel from A to B. The convex solution is to just take your car: The cost (as say measured in time) scales pretty much linearly in the distance, and you will simply take the shortest route. If you look at the region you can reach in a given time, you get some convex region -- essentially a circle. The nonconvex solution is to first walk to the bus station, then take the bus to the train station, then take the train to the airport, then fly, and finally reverse those steps. The set of points you can reach via this method in a given time is highly nonconvex. So you are taking steps of widely different scales (in the math: the different powers $T^n$ of $T$), but their cost (as measured in time, in the math: $|T^n|=r^n$) is not proportional to the scale ($T^n\mapsto 10^{-n}\in \mathbb R$). On the other hand, within each scale you would again take the shortest route. Each scale itself is discretized (most evidently in case of bus stations, train stations and airports).
So what we ended up doing is to prove the analogue of the desired theorem over $\mathbb Z((T))_r$ instead, see Theorem 9.1 here. It's a bit hard to summarize the argument and I don't have a clear sense of what's the key argument, but I currently believe it is precisely this reduction of a nonconvex problem to discrete convex problems on different scales. Now this kind of stuff is way out of my area of expertise, so I very naively wonder whether this is in fact a well-known technique, leading me to my
Main Question: Is the reduction of a nonconvex problem to a discrete convex problem (e.g. via using different scales) a well-known technique?
My traveling analogy makes me think the answer must evidently be "Yes", but I'd be happy to see some references. I'd be especially interested if there are any previous instances where questions on real functional analysis have been proved via passage to an arithmetic ring like $\mathbb Z((T))_r$, but all answers or pointers are most welcome.
Edit: Thanks for the comments so far! My naive googling about multiscale methods or so mostly lead me to very applied things. This is not bad, but I just wanted to remark that the method we use seems to be mostly of theoretical value -- a back-of-the-envelope calculation suggests that in our proof, under this analogy, the number of bus stations, train stations, and airports has to be roughly doubly exponential in some natural parameters that occur ;-). Now I believe there's also a lot of pure work using multiscale arguments, I just don't really know where to start looking.