DivisorFactorBound.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem337.truncatedDivisorCount line 9
Source documentation
Number of positive divisors at most a real cutoff.
```
def truncatedDivisorCount (X : ℝ) (n : ℕ) : ℕ :=
…
```
theorem OAI.Problem337.divisor_gcd_pair_injective line 13
Source documentation
Splitting a divisor at its gcd with a fixed factor loses no information.
```
theorem divisor_gcd_pair_injective (d : ℕ) :
    Function.Injective (fun a : ℕ => (Nat.gcd a d, a / Nat.gcd a d)) := by
…
```
theorem OAI.Problem337.divisor_div_gcd_dvd_quotient line 20
Source documentation
The factor remaining after taking a gcd divides the complementary factor.
```
theorem divisor_div_gcd_dvd_quotient {a d n : ℕ} (ha : a ∣ n) (hd : d ∣ n) :
    a / Nat.gcd a d ∣ n / d := by
…
```
theorem OAI.Problem337.truncatedDivisorCount_factor_bound line 30
Source documentation
The truncated divisor count is submultiplicative across any factorization; the factors need not be coprime.
```
theorem truncatedDivisorCount_factor_bound (X : ℝ) {d n : ℕ} (hd : d ∣ n) :
    truncatedDivisorCount X n ≤ d.divisors.card * truncatedDivisorCount X (n / d) := by
…
```
Mentions: OAI.Problem337.truncatedDivisorCount