Finite arithmetic progressions

Stream: Is there code for X?

[Jukka Kohonen]

Is there code for finite arithmetic progressions? Either as lists or (preferably) finite sets, such as {5,7,9,11} (4 integers starting from 5 with step 2). I know of data.finset.intervals which seems very handy, but only has "step 1" progressions. I would need these for results in finite additive combinatorics. Obviously I can create a step-s progression by taking an interval of integers and multiplying pointwise by s, but next I will be needing results on sums and cardinalities of such beasts.

[Eric Wieser]

docs#linear_recurrence? edit: no, that's not for arithmetic progressions

[Eric Wieser]

It seem a little strange to me to represent progressions as a set rather than a list or tuple, since progressions seem inherently ordered

[Eric Wieser]

The tuple version could look like this:

import data.fin.vec_notation

#eval (λ x : fin 4, 5 + 3*↑x)
-- ![5, 8, 11, 14]

[Jukka Kohonen]

I don't have any strong preference between set and list here. What I essentially need is ability to form pointwise sums and have some characterization of the result (e.g. adding two progressions that have the same step is a new progression with the same step, and we know its endpoints and cardinality).

[Eric Wieser]

You want to do pointwise sums of sequences that are the same length, right?

[Eric Wieser]

In that case, tuples are a better fit for you than lists or sets, as:

#eval (λ x : fin 4, 5 + 3*↑x) + (λ x : fin 4, 1 + 2*↑x)
-- ![6, 11, 16, 21]

[Jukka Kohonen]

No, different lengths, "pointwise" really meaning "pairwise" as in data.finset.pointwise. We call these sumsets in additive combinatorics. For example {1,2,3} + {40,50} = {41,42,43,51,52,53}.

[Kevin Buzzard]

So you probably don't want to use lists for that

[Jukka Kohonen]

I do have some rudimentary code already, based on data.finset.Ico and multiplying by the steplength, but then I thought I may be reinventing the wheel. But perhaps not?

[Eric Wieser]

This might be a nice way to formulate it (assuming its true!)

/-- `seq step (n, start)` is a sequence of `n.succ` terms starting at `start` -/
def seq {R} [semiring R] [decidable_eq R] (step : R) : (ℕ × R) →+ (finset R) :=
{ to_fun := λ p, (finset.range p.1.succ).image (λ i, p.1 + i • step),
  map_zero' := begin
    simp,
    refl,
  end,
  map_add' := λ x y, begin
    simp_rw [prod.fst_add, ←nat.succ_add, finset.range_add, nat.cast_add,
      finset.image_union, finset.map_eq_image, finset.image_image],
   sorry
  end }

You can then use (seq step).mrange to talk about the set of sequences of a fixed step, which are closed under addition

[Jukka Kohonen]

An example of an auxiliary result I'm trying to prove: If A is a progression with step length s, and B is an interval of at least s consecutive integers, then the sumset A+B is a specific interval. (Borrowing Matlab notation for an example: the sumset of 100:10:200 and 0:9 is exactly the interval 100:209.) Next I'll generalize to both A and B having steplengths greater than 1, etc.

[Eric Wieser]

Ah, if you're mixing step sizes then my suggestion above is also probably not helpful (other than perhaps (finset.range n.succ).image (λ i, start + i • step) being a useful spelling)

[Jukka Kohonen]

Thanks Eric! I think this suggestion essentially leads to something similar as my original idea of multiplying intervals with constants like {s} * (finset.Ico a a+l). In both cases I get finsets with whatever tools already exist for them. Intervals have "pointwise" addition already.

[Eric Wieser]

Note that when a is not a nat those mean different things

[Eric Wieser]

That is, if R is "the integer multiples of 1/2" and a : R, then (finset.Ico a a+l) will produce 2*l items

[Jukka Kohonen]

Yes, cardinalities of intervals will be heavily dependent on the element type, I'll have to be careful with that. For my own purposes the elements will be integers or vectors of integers, but for generality...

[Eric Wieser]

Regarding vector of integers; note that finset.Ico ![0, 0] ![1, 1] is {![0, 0], ![1, 0], ![0, 1]} (docs#pi.locally_finite_order)

[Yaël Dillies]

Hey, welcome! What are you trying to formalize? I've been working a lot on data.finset.pointwise to prepare for Plünnecke and Freiman's theorem.

[Yaël Dillies]

Relatingly, @Bhavik Mehta and I already have Roth's theorem on a branch, but we cheated because we didn't need a predicate for arbitrary arithmetic progressions, just arithmetic progressions of length 3, so we settled on docs#add_salem_spencer.

[Yaël Dillies]

Bhavik also has a proof that $|A| + |B| - 1 ≤ |A + B|$ but I don't remember what he used as a predicate.

[Jukka Kohonen]

I'm trying to formalize efficiency results on additive bases, basically, how many consecutive integers you can cover by the sumset A+A when cardinality |A¦ is fixed. Generic lower bounds (= you can cover at least this many integers, parameterized by |A|) are proven by explicit constructions where A is a union of arithmetic progressions (of different step sizes). The coverage of consecutive integers is essential in this context.

[Jukka Kohonen]

So this is slightly aside from typical arithmetic combinatorics because we are not looking at the cardinality of the sumset as such. We are trying to maximize the coefficient $c=n/k^2$ where n is the length of the interval covered by $A+A$, and $k=|A|$. A classical construction for $c=1/4$ is very simple, it is a union of two arithmetic progressions (with different steps). I believe the most recent is $c=85/294$ by myself in https://arxiv.org/abs/1606.04770 using a union of 42 progressions.

[Eric Wieser]

(note math is $$double dollars$$: $\LaTeX$)

[Yaël Dillies]

Oh that's very cool! And that also means we won't step on each other's toes :grinning:

[Jukka Kohonen]

:grinning: Indeed fixed-length progressions (e.g. three) can be handled pretty smoothly compared to these parameterized-length ones. Anyway if someone comes up with a very smooth representation of arbitrary-length progressions (with a wonderful API for sumsets and coverage) I'd love to hear. Meanwhile I'll be stumbling ahead with my homebrew representation...

[Yaël Dillies]

I will have to write this API for myself in the next month or two, so watch out!

[Jukka Kohonen]

@Yaël Dillies Did you by any chance do something on this? I've been doind other things but now possibly going to continue my additive-basis efforts.

[Yaël Dillies]

@Jukka Kohonen, I owe you an update: I have been working on the Kelley-Meka bound on Roth numbers over at https://github.com/YaelDillies/LeanAPAP and there I only need arithmetic progressions of length 3, so I haven't yet developed the API you wanted.