DivisorGraphSupport.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Arithmetic support of the unequal-coefficient graph edges

theorem OAI.JointDickman.coprime_of_divisor_linear_succ line 11
theorem OAI.JointDickman.amplificationInnerWeight_support line 19

theorem OAI.JointDickman.divisor_pair_small_lag line 35

Source documentation

Both congruences and the coefficient window force a small nonzero lag.

theorem divisor_pair_small_lag {T a b c m : ℕ}
    (ha : c ∣ a*m+1) (hb : c ∣ b*m+1) (hab : a ≠ b)
    (hwa : T*c < a ∧ a < 2*(T*c)) (hwb : T*c < b ∧ b < 2*(T*c)) :
    ∃ j : ℤ, j ≠ 0 ∧ (a : ℤ)-b = j*c ∧ j.natAbs < T := by
…

theorem OAI.JointDickman.auxiliaryProduct_coprime_small line 59
Source documentation
A prime-product coefficient is coprime to every nonzero small lag.
```
theorem auxiliaryProduct_coprime_small {B : ℕ} {A : Finset ℕ}
    (hA : A ⊆ auxiliaryPrimes B) {d : ℕ} (hd : 0 < d)
    (hdsmall : d ≤ auxiliaryCutoff B) : (∏ p ∈ A, p).Coprime d := by
…
```
Mentions: OAI.JointDickman.auxiliaryPrimes, OAI.JointDickman.auxiliaryCutoff
theorem OAI.JointDickman.divisor_edge_coprime line 75
Source documentation
Once the coefficient is coprime to the lag and to c, the edge's two coefficients are coprime. This is the cancellation used by the inverse map.
```
theorem divisor_edge_coprime {a b c : ℕ} {j : ℤ}
    (hac : a.Coprime c) (haj : a.Coprime j.natAbs)
    (he : (a : ℤ)-b = j*c) : a.Coprime b := by
…
```