SmoothInclusionExclusion.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Exact finite inclusion-exclusion for smoothness

For a finite set of distinct primes, expand the product of their avoidance indicators and count multiples of each squarefree prime product. The result is an exact identity; no prime asymptotic or correlation input is used here.

def OAI.JointDickman.excludedPrimeCount line 21
Source documentation
The integers 1 ≤ n ≤ N with no factor among the excluded primes.
```
noncomputable def excludedPrimeCount (E : Finset ℕ) (N : ℕ) : ℕ := by
…
```
theorem OAI.JointDickman.primeProduct_dvd_iff line 25
Distinct definitions of this name: OAI/NumberTheory/JointDickman/Analysis/MellinSieveRemainder.lean:12 (different declaration text), OAI/NumberTheory/JointDickman/Arithmetic/DivisorProductMean.lean:13 (different declaration text). Qualify references as OAI.JointDickman.primeProduct_dvd_iff@path.
theorem OAI.JointDickman.avoidance_indicator line 32
theorem OAI.JointDickman.divisor_indicator_product line 46

theorem OAI.JointDickman.prime_avoidance_inclusion_exclusion line 62

Source documentation

The finite inclusion-exclusion identity before averaging.

theorem prime_avoidance_inclusion_exclusion (E : Finset ℕ)
    (hE : ∀ p ∈ E, p.Prime) (n : ℕ) :
    (if ∀ p ∈ E, ¬p ∣ n then (1 : ℝ) else 0) =
      ∑ s ∈ E.powerset, (-1 : ℝ) ^ s.card *
        (if (∏ p ∈ s, p) ∣ n then 1 else 0) := by
…

theorem OAI.JointDickman.sum_divisor_indicator line 75
theorem OAI.JointDickman.excludedPrimeCount_eq_inclusion_exclusion line 82
Source documentation
The exact floor formula for integers avoiding a finite set of primes. Natural division on the right is floor(N / product(s)).
```
theorem excludedPrimeCount_eq_inclusion_exclusion (E : Finset ℕ)
    (hE : ∀ p ∈ E, p.Prime) (N : ℕ) :
    (excludedPrimeCount E N : ℝ) =
      ∑ s ∈ E.powerset, (-1 : ℝ) ^ s.card * (N / (∏ p ∈ s, p) : ℕ) := by
…
```
Mentions: OAI.JointDickman.excludedPrimeCount
def OAI.JointDickman.excludedSmoothnessPrimes line 108
Source documentation
The primes that prevent an integer up to N from being y-smooth.
```
noncomputable def excludedSmoothnessPrimes (N : ℕ) (y : ℝ) : Finset ℕ := by
…
```

theorem OAI.JointDickman.maxPrimeFac_le_iff_avoids_excluded line 113

Source documentation

On 1 ≤ n ≤ N, avoidance of the finite excluded set is smoothness.

theorem maxPrimeFac_le_iff_avoids_excluded {N n : ℕ} {y : ℝ}
    (hy : 1 ≤ y) (hn : 1 ≤ n) (hnN : n ≤ N) :
    (n.maxPrimeFac : ℝ) ≤ y ↔ ∀ p ∈ excludedSmoothnessPrimes N y, ¬p ∣ n := by
…

Mentions: OAI.JointDickman.excludedSmoothnessPrimes

theorem OAI.JointDickman.smoothCount_eq_inclusion_exclusion line 134

Source documentation

The exact inclusion-exclusion formula for the ordinary smooth count.

theorem smoothCount_eq_inclusion_exclusion (N : ℕ) (y : ℝ) (hy : 1 ≤ y) :
    (((Finset.Ioc 0 N).filter (fun n => (n.maxPrimeFac : ℝ) ≤ y)).card : ℝ) =
      ∑ s ∈ (excludedSmoothnessPrimes N y).powerset,
        (-1 : ℝ) ^ s.card * (N / (∏ p ∈ s, p) : ℕ) := by
…

Mentions: OAI.JointDickman.excludedSmoothnessPrimes