IntegerProgressionPartition.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Exact residue-progressions in a padded integer interval

def OAI.Ostmann.integerProgressionPartition line 11
Source documentation
Row/column transposition lists each residue class in increasing order.
```
def integerProgressionPartition (Q K : ℕ) : Fin (K * Q) ≃ Σ _ : Fin Q, Fin K :=
…
```
theorem OAI.Ostmann.integerProgressionPartition_value line 15
theorem OAI.Ostmann.integerProgressionPartition_padding line 22
Source documentation
An interval can be padded by at most one modulus to get this exact rectangular decomposition; original support indicators can retain its endpoints.
```
theorem integerProgressionPartition_padding (N Q : ℕ) (hQ : 0 < Q) :
    N < (N / Q + 1) * Q ∧ (N / Q + 1) * Q ≤ N + Q := by
…
```

theorem OAI.Ostmann.integerProgressionPartition_sum line 32

Source documentation

Reindexing the original integer sum introduces neither missing boundary integers nor multiplicity.

theorem integerProgressionPartition_sum {M : Type*} [AddCommMonoid M]
    (Q K : ℕ) (f : Fin (K * Q) → M) :
    (∑ x, f x) = ∑ r : Fin Q, ∑ j : Fin K,
      f ((integerProgressionPartition Q K).symm ⟨r, j⟩) := by
…

Mentions: OAI.Ostmann.integerProgressionPartition