TruncatedDivisors.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem337.DivisorMoment.truncatedDivisors line 7
Source documentation
Positive divisors truncated at an integral threshold.
```
def truncatedDivisors (X n : ℕ) : Finset ℕ :=
…
```
theorem OAI.Problem337.DivisorMoment.mem_truncatedDivisors line 10
theorem OAI.Problem337.DivisorMoment.div_gcd_dvd_quotient line 16
Source documentation
The second component of the gcd splitting is a divisor of the quotient. No coprimality of the chosen factor and the quotient is needed.
```
theorem div_gcd_dvd_quotient {a d n : ℕ} (ha : a ∣ n) (hd : d ∣ n) :
    a / Nat.gcd a d ∣ n / d := by
…
```
theorem OAI.Problem337.DivisorMoment.gcd_split_injective line 26
Source documentation
Divisor splitting is injective, because its components multiply to the input.
```
theorem gcd_split_injective (d : ℕ) :
    Function.Injective (fun a : ℕ => (Nat.gcd a d, a / Nat.gcd a d)) := by
…
```
theorem OAI.Problem337.DivisorMoment.truncated_card_le_mul line 35
Source documentation
Truncated divisors of a product inject into a full divisor set and one truncated divisor set. This is the prefix inequality in the divisor moment argument.
```
theorem truncated_card_le_mul {X n d : ℕ} (hn : 0 < n) (hd : d ∣ n) :
    (truncatedDivisors X n).card ≤
      d.divisors.card * (truncatedDivisors X (n / d)).card := by
…
```
Mentions: OAI.Problem337.DivisorMoment.truncatedDivisors
theorem OAI.Problem337.DivisorMoment.interval_multiples_card_le line 54
Source documentation
Multiples of a positive integer in a translated interval satisfy the uniform counting estimate needed for short-interval divisor moments.
```
theorem interval_multiples_card_le (N Y d : ℕ) (hd : 0 < d) :
    ((Finset.Ioc N (N + Y)).filter (fun a => d ∣ a)).card ≤ Y / d + 1 := by
…
```
theorem OAI.Problem337.DivisorMoment.interval_multiples_card_le_real line 79
theorem OAI.Problem337.DivisorMoment.interval_multiples_card_le_twice line 90

theorem OAI.Problem337.DivisorMoment.interval_multiples_real_cutoff line 105

Source documentation

Real lengths are implemented by their natural floor, without changing the uniform interval bound.

theorem interval_multiples_real_cutoff (N d : ℕ) (Y : ℝ) (hY : 0 ≤ Y)
    (hd : 0 < d) :
    (((Finset.Ioc N (N + ⌊Y⌋₊)).filter (fun a => d ∣ a)).card : ℝ) ≤
      Y / d + 1 := by
…

theorem OAI.Problem337.DivisorMoment.interval_multiples_real_cutoff_twice line 115