PrimePowerMoments.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Logarithmic multiplicities and moments of products of finitely many prime powers.

lemma OAI.CubicFirstMoment.idealExponentOf_one line 14
lemma OAI.CubicFirstMoment.idealExponentOf_primePower_card line 17
lemma OAI.CubicFirstMoment.primary_prime_pow line 29
lemma OAI.CubicFirstMoment.idealExponentOf_prod_card line 34
lemma OAI.CubicFirstMoment.orderedPrimePowerSupport_spec line 47
lemma OAI.CubicFirstMoment.natLog_power_bound line 67
Source documentation
A fixed logarithmic power is bounded by every positive norm power, with an explicit constant uniform down to norm one.
```
lemma natLog_power_bound (m : ℕ) {ε : ℝ} (hε : 0 < ε) :
    ∃ C : ℝ, 0 < C ∧ ∀ n : ℕ, 1 ≤ n →
      ((Nat.log 2 n + 1 : ℕ) : ℝ)^m ≤ C*(n:ℝ)^ε := by
…
```
lemma OAI.CubicFirstMoment.boundedPrimeSupport_pair_fiber_power line 106

theorem OAI.CubicFirstMoment.boundedPrimeSupport_fourth_moment line 137

Source documentation

Actual fourth moments for supports with a bounded number of prime bases. The arbitrary higher powers cost only an arbitrarily small norm power.

theorem boundedPrimeSupport_fourth_moment (hHuxley : HuxleyAdditiveLargeSieve)
    (k : ℕ) {ε : ℝ} (hε : 0 < ε) :
    ∃ C : ℝ, 0 < C ∧ ∀ (Q Y : ℝ), 1 ≤ Q → 1 ≤ Y →
      ∀ (P : Finset (Eisenstein × Eisenstein)) (B : Finset Eisenstein),
      (∀ p ∈ P, PrimarySquarefreePair p ∧ norm (pairConductor p) ≤ Q) →
      (∀ b ∈ B, primary b ∧ norm b ≤ Y ∧ (idealExponentOf b).support.card ≤ k) →
      ∀ v : Eisenstein → ℂ,
      (∑ p ∈ P, ‖∑ b ∈ B, v b*mixedCubic p.1 p.2 b‖^4) ≤
        C*Q^ε*(Q^2+Y^2)*Y^ε*(∑ b ∈ B, ‖v b‖^2)^2 := by
…

Mentions: OAI.CubicFirstMoment.HuxleyAdditiveLargeSieve, OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.PrimarySquarefreePair, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.pairConductor, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.idealExponentOf, OAI.CubicFirstMoment.mixedCubic