Besicovitch satellites

Stream: general

[Yaël Dillies]

We're trying to prove Solymosi's proof of Elekes' bound for the sum-product problem. docs#besicovitch.satellite_config supposes an order on the balls which makes it hard to use for us. @Sebastien Gouezel, what do you think of renaming besicovitch.satellite_config to besicovitch.satellite_config_aux and define besicovitch.satellite_config as the unordered equivalent. Then one can easily show that for 1 ≤ τ having a satellite_config is the same as having a satellite_config_aux.

[Sebastien Gouezel]

No objection there. I am not sure what you mean by an order of the balls (the only ball that is special is the last one, otherwise they are all interchangeable). But I am not attached to the details of the definition, my main interest was to use it to prove the Besicovitch covering theorem in normed spaces. So if the theorem is still there in the end you can make any modification you like.

[Yaël Dillies]

You're taking in balls indexed by fin n, which induces an ordering (and in our case means we have to reindex our family of balls, which is painful). Thanks, I'll PR the modification soonish!