AdditionProgressionGeometry.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The actual progression of numeric additions

theorem OAI.JointDickman.auxiliary_product_coprime_lag line 13
Source documentation
Every selected coefficient is a unit modulo an allowed lag.
```
theorem auxiliary_product_coprime_lag {B j : ℕ} {A : Finset ℕ}
    (hA : A ⊆ auxiliaryPrimes B) (hj : 0 < j) (hcut : j ≤ auxiliaryCutoff B) :
    (∏ p ∈ A, p : ℕ).Coprime j := by
…
```
Mentions: OAI.JointDickman.auxiliaryPrimes, OAI.JointDickman.auxiliaryCutoff
theorem OAI.JointDickman.addition_equation_modEq line 24
Source documentation
Once the retained factors and the other addition are fixed, two valid numeric additions have the same residue modulo the lag.
```
theorem addition_equation_modEq {e j b z w c d : ℕ} (hej : e.Coprime j)
    (hz : e*z = b+j*c) (hw : e*w = b+j*d) : Nat.ModEq j z w := by
…
```

theorem OAI.JointDickman.addition_equation_progression line 34

Source documentation

A nonempty coefficient class has one residue z₀ and one integral intercept c₀. Every other member is z=z₀+jt, c=c₀+et with t=z/j.

theorem addition_equation_progression {e j b w d : ℕ} (hj : 0 < j) (hej : e.Coprime j)
    (hw : e*w = b+j*d) :
    ∃ (z₀ : ℕ) (c₀ : ℤ), z₀ < j ∧
      (e : ℤ)*z₀ = b+(j : ℤ)*c₀ ∧
      ∀ (z c : ℕ), e*z = b+j*c →
        z = z₀+j*(z/j) ∧ (c : ℤ) = c₀+(e : ℤ)*((z/j : ℕ) : ℤ) := by
…

theorem OAI.JointDickman.addition_progression_determinant line 65
Source documentation
The determinant of the two progression forms is the fixed nonzero opposite coefficient, with no dependence on the progression variable.
```
theorem addition_progression_determinant {e j b z₀ : ℕ} {c₀ : ℤ}
    (hbase : (e : ℤ)*z₀ = b+(j : ℤ)*c₀) :
    (z₀ : ℤ)*e-c₀*j = b := by linear_combination hbase
…
```