PrimeSeparation.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Large-prime divisor counting

The prime-divisor counting estimate gives the arithmetic step in the finite-tree separation induction, prop:finite-separation.

theorem OAI.TreeEdit.BinaryLower.PrimeSeparation.card_filter_dvd_lt line 18

Source documentation

Fewer than q distinct primes at least L can divide a positive integer smaller than L ^ q. The indexing set need not be all of a type.

theorem card_filter_dvd_lt {ι : Type*} [DecidableEq ι]
    (s : Finset ι) (p : ι → ℕ) (L q n : ℕ)
    (hp : ∀ i ∈ s, (p i).Prime)
    (hinj : Set.InjOn p (s : Set ι))
    (hL : ∀ i ∈ s, L ≤ p i)
    (hLpos : 0 < L) (hnpos : 0 < n) (hn : n < L ^ q) :
    (s.filter fun i => p i ∣ n).card < q := by
…

theorem OAI.TreeEdit.BinaryLower.PrimeSeparation.card_filter_int_dvd_lt line 45

Source documentation

Integer form of card_filter_dvd_lt, with no sign restriction.

theorem card_filter_int_dvd_lt {ι : Type*} [DecidableEq ι]
    (s : Finset ι) (p : ι → ℕ) (L q : ℕ) (z : ℤ)
    (hp : ∀ i ∈ s, (p i).Prime)
    (hinj : Set.InjOn p (s : Set ι))
    (hL : ∀ i ∈ s, L ≤ p i)
    (hLpos : 0 < L) (hz : z ≠ 0) (hsmall : z.natAbs < L ^ q) :
    (s.filter fun i => (p i : ℤ) ∣ z).card < q := by
…

theorem OAI.TreeEdit.BinaryLower.PrimeSeparation.finite_tree_few_prime_divisors line 58

Source documentation

The numerical divisor estimate used for two different rows of the finite construction (T = k^(20*k), primes at least k^4).

theorem finite_tree_few_prime_divisors {ι : Type*} [DecidableEq ι]
    (s : Finset ι) (p : ι → ℕ) (k : ℕ) (z : ℤ)
    (hk : 2 ≤ k) (hp : ∀ i ∈ s, (p i).Prime)
    (hinj : Set.InjOn p (s : Set ι))
    (hlarge : ∀ i ∈ s, k ^ 4 ≤ p i)
    (hz : z ≠ 0) (hsmall : z.natAbs < k ^ (20 * k)) :
    (s.filter fun i => (p i : ℤ) ∣ z).card < 10 * k := by
…

theorem OAI.TreeEdit.BinaryLower.PrimeSeparation.finite_tree_many_nondividing_children line 76

Source documentation

At least half of the children have periods not dividing the relative shift between different rows. Q is arbitrary here; the product R forces each child prime to divide the distinguished-shift contribution.

theorem finite_tree_many_nondividing_children
    (k Q : ℕ) (p : Fin (20 * k) → ℕ) (z t : ℤ)
    (hk : 2 ≤ k) (hp : ∀ i, (p i).Prime)
    (hinj : Function.Injective p) (hlarge : ∀ i, k ^ 4 ≤ p i)
    (hz : z ≠ 0) (hsmall : z.natAbs < k ^ (20 * k)) :
    10 * k ≤ (Finset.univ.filter fun i =>
      ¬ ((Q * p i : ℕ) : ℤ) ∣ z + t * (∏ j, p j : ℕ)).card := by
…

theorem OAI.TreeEdit.BinaryLower.PrimeSeparation.not_child_period_dvd_mul line 113
Source documentation
For the same row on both sides, coprimality of the parent period and R prevents every child period from dividing the distinguished shift.
```
theorem not_child_period_dvd_mul (Q R p : ℕ) (t : ℤ)
    (hcop : Nat.Coprime Q R) (ht : ¬ (Q : ℤ) ∣ t) :
    ¬ ((Q * p : ℕ) : ℤ) ∣ t * (R : ℤ) := by
…
```

theorem OAI.TreeEdit.BinaryLower.PrimeSeparation.finite_tree_row_pair_nondivisibility line 126

Source documentation

Complete row-pair arithmetic in Proposition prop:finite-separation. Every pair of legal row indices has at least m/2 = 10*k children for which the relative shift is nonzero modulo the child period.

theorem finite_tree_row_pair_nondivisibility
    (k Q : ℕ) (p : Fin (20 * k) → ℕ) (a b : ℕ) (t : ℤ)
    (hk : 2 ≤ k) (hp : ∀ i, (p i).Prime)
    (hinj : Function.Injective p) (hlarge : ∀ i, k ^ 4 ≤ p i)
    (ha : a < k ^ (20 * k)) (hb : b < k ^ (20 * k))
    (hcop : Nat.Coprime Q (∏ j, p j)) (ht : ¬ (Q : ℤ) ∣ t) :
    10 * k ≤ (Finset.univ.filter fun i =>
      ¬ ((Q * p i : ℕ) : ℤ) ∣
        (b : ℤ) - a + t * (∏ j, p j : ℕ)).card := by
…