GoldbachSieveRootBounds.lean`

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

instance OAI.Problem337.goldbachSieveRootFintype line 10
instance OAI.Problem337.goldbachSieveRootNonempty line 14
def OAI.Problem337.goldbachSieveRootLCMEmbedding line 19
Source documentation
Reduction modulo two possibly noncoprime moduli is injective when the source modulus is their least common multiple. This remains true on roots.
```
def goldbachSieveRootLCMEmbedding (u a b : ℕ) :
    GoldbachSieveRoot u (a.lcm b) ↪
      GoldbachSieveRoot u a × GoldbachSieveRoot u b := by
…
```
Mentions: OAI.Problem337.GoldbachSieveRoot
theorem OAI.Problem337.goldbachSieveRootCount_lcm_le line 41
Source documentation
LCM-submultiplicativity of the root count. This needs no squarefreeness.
```
theorem goldbachSieveRootCount_lcm_le (u a b : ℕ) [NeZero a] [NeZero b] :
    goldbachSieveRootCount u (a.lcm b) ≤
      goldbachSieveRootCount u a * goldbachSieveRootCount u b := by
…
```
Mentions: OAI.Problem337.goldbachSieveRootCount
theorem OAI.Problem337.goldbachSieveRootCount_pos line 50
Source documentation
Zero is always a root, so each positive modulus has positive local count.
```
theorem goldbachSieveRootCount_pos (u d : ℕ) [NeZero d] :
    0 < goldbachSieveRootCount u d := by
…
```
Mentions: OAI.Problem337.goldbachSieveRootCount
theorem OAI.Problem337.goldbachSieveRootCount_le line 55
Source documentation
The local root count cannot exceed the modulus.
```
theorem goldbachSieveRootCount_le (u d : ℕ) [NeZero d] :
    goldbachSieveRootCount u d ≤ d := by
…
```
Mentions: OAI.Problem337.goldbachSieveRootCount
theorem OAI.Problem337.goldbachSieveRootCount_eq_two_pow line 64
Source documentation
Exact exponent of two in a squarefree local root count.
```
theorem goldbachSieveRootCount_eq_two_pow (u d : ℕ) (hd : Squarefree d) :
    goldbachSieveRootCount u d =
      2 ^ (d.primeFactors.filter (fun p => ¬p ∣ u)).card := by
…
```
Mentions: OAI.Problem337.goldbachSieveRootCount
theorem OAI.Problem337.goldbachSieveRootCount_le_two_pow line 78
Source documentation
Squarefree local root counts are bounded by the number of subsets of prime factors, uniformly in the target.
```
theorem goldbachSieveRootCount_le_two_pow (u d : ℕ) (hd : Squarefree d) :
    goldbachSieveRootCount u d ≤ 2 ^ d.primeFactors.card := by
…
```
Mentions: OAI.Problem337.goldbachSieveRootCount