NonzeroGraphAtoms.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Nonzero summands give genuine coprime small-lag graph edges

theorem OAI.JointDickman.firstFormAtom_nonzero_support line 11

theorem OAI.JointDickman.nonzero_atoms_small_coprime_lag line 29

Source documentation

The actual nonzero atoms satisfy every arithmetic condition used in the change of variables. Distinct subsets give distinct coefficient integers.

theorem nonzero_atoms_small_coprime_lag {B L T : ℕ} (τ C : ℝ) (J : ℕ → ℂ)
    (N : ℕ) {D A E : Finset ℕ} (_hD : D ⊆ auxiliaryPrimes B)
    (hA : A ⊆ auxiliaryPrimes B) (hE : E ⊆ auxiliaryPrimes B) (hAE : A ≠ E)
    (hT : T ≤ auxiliaryCutoff B) (m : ℕ)
    (ha : firstFormAtom B L τ C (amplificationInnerWeight T) J N D m A ≠ 0)
    (hb : firstFormAtom B L τ C (amplificationInnerWeight T) J N D m E ≠ 0) :
    ∃ j : ℤ, j ≠ 0 ∧ j.natAbs < T ∧
      ((∏ p ∈ A, p : ℕ) : ℤ) - (∏ p ∈ E, p : ℕ) = j*(∏ p ∈ D, p : ℕ) ∧
      (∏ p ∈ A, p).Coprime (∏ p ∈ E, p) ∧
      (∏ p ∈ A, p).Coprime (∏ p ∈ D, p) ∧
      (∏ p ∈ E, p).Coprime (∏ p ∈ D, p) ∧
      (∏ p ∈ A, p).Coprime j.natAbs ∧ (∏ p ∈ E, p).Coprime j.natAbs := by
…

Mentions: OAI.JointDickman.auxiliaryPrimes, OAI.JointDickman.auxiliaryCutoff, OAI.JointDickman.firstFormAtom, OAI.JointDickman.amplificationInnerWeight

theorem OAI.JointDickman.amplificationMultiplier_le_cutoff line 53
Source documentation
The prescribed multiplier is eventually below the lower prime cutoff.
```
theorem amplificationMultiplier_le_cutoff : ∀ᶠ B : ℕ in atTop,
    amplificationMultiplier B ≤ auxiliaryCutoff B := by
…
```
Mentions: OAI.JointDickman.amplificationMultiplier, OAI.JointDickman.auxiliaryCutoff