RoughPart.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem337.roughPart line 11
Source documentation
The part of an integer supported on primes at least R, retaining their full multiplicities. The definition at zero is harmlessly the empty product.
```
def roughPart (R : ℝ) (n : ℕ) : ℕ :=
…
```
theorem OAI.Problem337.roughPart_pos line 14
theorem OAI.Problem337.roughPart_dvd line 19
theorem OAI.Problem337.roughPart_le line 25
theorem OAI.Problem337.roughPart_log_le line 28
theorem OAI.Problem337.roughPart_primeFactorsList line 33
theorem OAI.Problem337.roughPart_large line 39
theorem OAI.Problem337.dvd_roughPart_iff line 47
Source documentation
Divisibility in the rough part is exactly divisibility in the original integer together with the roughness of the divisor, not of the ambient integer.
```
theorem dvd_roughPart_iff (R : ℝ) {n d : ℕ} (hn : n ≠ 0) :
    d ∣ roughPart R n ↔ d ∣ n ∧ ∀ p ∈ d.primeFactorsList, R ≤ (p : ℝ) := by
…
```
Mentions: OAI.Problem337.roughPart

theorem OAI.Problem337.rough_divisors_eq_roughPart_divisors line 69

Source documentation

Exact finite-set transport, including all repeated prime powers.

theorem rough_divisors_eq_roughPart_divisors (R X : ℝ) {n : ℕ} (hn : n ≠ 0) :
    n.divisors.filter (fun d : ℕ => (d : ℝ) ≤ X ∧
      ∀ p ∈ d.primeFactorsList, R ≤ (p : ℝ)) =
    (roughPart R n).divisors.filter (fun d : ℕ => (d : ℝ) ≤ X) := by
…

Mentions: OAI.Problem337.roughPart

theorem OAI.Problem337.rough_divisor_card_le_truncated_roughPart line 86
Source documentation
Any finite family of rough divisors is bounded by the existing truncated count of the single rough part. This is the transport needed for differences of samples, whose small prime factors must not be excluded.
```
theorem rough_divisor_card_le_truncated_roughPart (R X : ℝ) {n : ℕ}
    (hn : n ≠ 0) (s : Finset ℕ)
    (hdiv : ∀ d ∈ s, d ∣ n)
    (hsmall : ∀ d ∈ s, (d : ℝ) ≤ X)
    (hrough : ∀ d ∈ s, ∀ p ∈ d.primeFactorsList, R ≤ (p : ℝ)) :
    s.card ≤ truncatedDivisorCount X (roughPart R n) := by
…
```
Mentions: OAI.Problem337.truncatedDivisorCount, OAI.Problem337.roughPart