PrimePowerDivisors.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Divisor and pair-product multiplicities with a bounded number of prime bases.

lemma OAI.CubicFirstMoment.idealExponentOf_inj_primary line 14
lemma OAI.CubicFirstMoment.idealExponentOf_le_of_dvd line 21
lemma OAI.CubicFirstMoment.primary_divisor_card_exponents line 28
lemma OAI.CubicFirstMoment.idealPrimeRepresentative_normNat_ge_two line 47
lemma OAI.CubicFirstMoment.idealExponentOf_le_log_norm line 59
theorem OAI.CubicFirstMoment.primary_divisor_card_log line 78
Source documentation
Only the number of distinct prime bases enters this bound; their exponents may be arbitrarily large.
```
theorem primary_divisor_card_log (T : Finset Eisenstein)
    (hT : ∀ a ∈ T, primary a) {b : Eisenstein} (hb : b ≠ 0) {k : ℕ}
    (hk : (idealExponentOf b).support.card ≤ k) :
    (T.filter (fun a => a ∣ b)).card ≤ (Nat.log 2 (normNat b) + 1)^k := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.idealExponentOf, OAI.CubicFirstMoment.normNat

lemma OAI.CubicFirstMoment.primary_pair_fiber_le_divisors line 90

Source documentation

For primary factors, fixing the first divisor determines the second.

lemma primary_pair_fiber_le_divisors (B : Finset Eisenstein)
    (hB : ∀ a ∈ B, primary a) (n : Eisenstein) :
    ((B.product B).filter (fun z => z.1*z.2 = n)).card ≤
      (B.filter (fun a => a ∣ n)).card := by
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary

lemma OAI.CubicFirstMoment.idealExponentOf_mul_support_card line 114
theorem OAI.CubicFirstMoment.boundedPrimeSupport_pair_fiber line 122
Source documentation
Pair-product fibers of elements with at most k prime bases cost only a 2k-th power of a logarithm, even for high prime powers.
```
theorem boundedPrimeSupport_pair_fiber (B : Finset Eisenstein)
    (hB : ∀ a ∈ B, primary a) (k : ℕ)
    (hk : ∀ a ∈ B, (idealExponentOf a).support.card ≤ k)
    {n : Eisenstein} (hn : n ∈ productSupport B) :
    ((B.product B).filter (fun z => z.1*z.2 = n)).card ≤
      (Nat.log 2 (normNat n) + 1)^(2*k) := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.idealExponentOf, OAI.CubicFirstMoment.productSupport, OAI.CubicFirstMoment.normNat