IdealDivisorPower.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Arbitrary-exponent ideal divisor bounds for the short-convolution polynomials. No bound on the number of distinct prime bases is assumed.

lemma OAI.CubicFirstMoment.idealExponentNorm_eq_prod line 12
lemma OAI.CubicFirstMoment.exponent_add_one_le_two_pow line 22
lemma OAI.CubicFirstMoment.exponent_factor_uniform line 31
theorem OAI.CubicFirstMoment.ideal_divisor_product_small_power line 54
Source documentation
The full ideal divisor product is bounded by every positive norm power. Small prime ideals form a finite set, while large prime ideals absorb every exponent directly.
```
theorem ideal_divisor_product_small_power {ε : ℝ} (hε : 0 < ε) :
    ∃ C : ℝ, 0 < C ∧ ∀ ν : EisensteinIdealExponent,
      (∏ p ∈ ν.support, ((ν p:ℝ)+1)) ≤ C*idealExponentNorm ν^ε := by
…
```
Mentions: OAI.CubicFirstMoment.EisensteinIdealExponent, OAI.CubicFirstMoment.idealExponentNorm
theorem OAI.CubicFirstMoment.primary_divisor_card_small_power line 118
Source documentation
Arbitrary primary divisors, with no squarefree or bounded-prime-support restriction on the ambient element.
```
theorem primary_divisor_card_small_power {ε : ℝ} (hε : 0 < ε) :
    ∃ C : ℝ, 0 < C ∧ ∀ (T : Finset Eisenstein),
      (∀ a ∈ T, primary a) → ∀ b : Eisenstein, b ≠ 0 →
      ((T.filter (fun a => a ∣ b)).card : ℝ) ≤ C*norm b^ε := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.norm