PrimePowerConvolution.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Actual prime-power convolution coefficients: bounded prime support absorbs all tuple multiplicities in an arbitrarily small norm power.

lemma OAI.CubicFirstMoment.orderedConvolution_eq_zero_of_not_mem line 14

theorem OAI.CubicFirstMoment.primePower_tuple_fiber_card line 25

Source documentation

A tuple with prescribed nonzero product chooses each coordinate among its primary divisors. Boundedly many prime bases give a logarithmic bound.

theorem primePower_tuple_fiber_card (S : ι → Finset Eisenstein)
    (hS : ∀ i, ∀ a ∈ S i, ∃ p : Eisenstein, ∃ j : ℕ,
      primaryPrime p ∧ 0 < j ∧ a = p^j) (b : Eisenstein) :
    ((Fintype.piFinset S).filter (fun f => (∏ i, f i) = b)).card ≤
      (Nat.log 2 (normNat b)+1)^((Fintype.card ι)*(Fintype.card ι)) := by
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primaryPrime, OAI.CubicFirstMoment.normNat

theorem OAI.CubicFirstMoment.primePower_orderedConvolution_norm_bound line 63

Source documentation

Actual independent weights, including arbitrary higher prime powers.

theorem primePower_orderedConvolution_norm_bound (S : ι → Finset Eisenstein)
    (w : ι → Eisenstein → ℂ) (M : ι → ℝ)
    (hS : ∀ i, ∀ a ∈ S i, ∃ p : Eisenstein, ∃ j : ℕ,
      primaryPrime p ∧ 0 < j ∧ a = p^j)
    (hM : ∀ i, 0 ≤ M i) (hw : ∀ i, ∀ a ∈ S i, ‖w i a‖ ≤ M i)
    (b : Eisenstein) :
    ‖orderedConvolution S w b‖ ≤
      (((Nat.log 2 (normNat b)+1)^((Fintype.card ι)*(Fintype.card ι)):ℕ):ℝ)*(∏ i, M i) := by
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primaryPrime, OAI.CubicFirstMoment.orderedConvolution, OAI.CubicFirstMoment.normNat

theorem OAI.CubicFirstMoment.primePower_orderedConvolution_smallPower line 88

Source documentation

The full coefficient multiplicity has arbitrary small-power growth, uniformly in the separate prime-power supports and weights.

theorem primePower_orderedConvolution_smallPower {ε : ℝ} (hε : 0 < ε) :
    ∃ C : ℝ, 0 < C ∧ ∀ (S : ι → Finset Eisenstein)
      (w : ι → Eisenstein → ℂ) (M : ι → ℝ),
      (∀ i, ∀ a ∈ S i, ∃ p : Eisenstein, ∃ j : ℕ,
        primaryPrime p ∧ 0 < j ∧ a = p^j) →
      (∀ i, 0 ≤ M i) → (∀ i, ∀ a ∈ S i, ‖w i a‖ ≤ M i) →
      ∀ (Y : ℝ), 1 ≤ Y → ∀ b ∈ orderedConvolutionSupport S, norm b ≤ Y →
      ‖orderedConvolution S w b‖ ≤ C*Y^ε*(∏ i, M i) := by
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primaryPrime, OAI.CubicFirstMoment.orderedConvolutionSupport, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.orderedConvolution

theorem OAI.CubicFirstMoment.primePowerConvolution_balanced_second_moment line 112

Source documentation

Actual collected higher-prime-power coefficients on the sparse error support satisfy the balanced moment. The only analytic input is Huxley.

theorem primePowerConvolution_balanced_second_moment
    (hHuxley : HuxleyAdditiveLargeSieve) {c : ℝ} (hc : 0 < c) (hc₁ : c ≤ 1) :
    ∃ C : ℝ, 0 < C ∧ ∀ (S : ι → Finset Eisenstein)
      (w : ι → Eisenstein → ℂ) (M : ι → ℝ),
      (∀ i, ∀ a ∈ S i, ∃ p : Eisenstein, ∃ j : ℕ,
        primaryPrime p ∧ 0 < j ∧ a = p^j) →
      (∀ i, 0 ≤ M i) → (∀ i, ∀ a ∈ S i, ‖w i a‖ ≤ M i) →
      ∀ Y : ℝ, 1 ≤ Y → ∀ P : Finset (Eisenstein × Eisenstein),
      (∀ p ∈ P, PrimarySquarefreePair p ∧
        norm p.1 ≤ Y^(1/3+c/128) ∧ norm p.2 ≤ Y^(1/3+c/128)) →
      ∀ χ : Eisenstein → ℂ,
      (∀ b ∈ (orderedConvolutionSupport S).filter
…

Mentions: OAI.CubicFirstMoment.HuxleyAdditiveLargeSieve, OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primaryPrime, OAI.CubicFirstMoment.PrimarySquarefreePair, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.orderedConvolutionSupport

theorem OAI.CubicFirstMoment.primePowerConvolution_first_shape_second_moment line 162

Source documentation

The first exceptional shape for the same actual prime-power convolution. The collected coefficient automatically vanishes outside its tuple support.

theorem primePowerConvolution_first_shape_second_moment
    {c : ℝ} (hc : 0 < c) (hc₁ : c ≤ 1) :
    ∃ C : ℝ, 0 < C ∧ ∀ (S : ι → Finset Eisenstein)
      (w : ι → Eisenstein → ℂ) (M : ι → ℝ),
      (∀ i, ∀ a ∈ S i, ∃ p : Eisenstein, ∃ j : ℕ,
        primaryPrime p ∧ 0 < j ∧ a = p^j) →
      (∀ i, 0 ≤ M i) → (∀ i, ∀ a ∈ S i, ‖w i a‖ ≤ M i) →
      ∀ Y : ℝ, 1 ≤ Y → ∀ P Q : Finset Eisenstein,
      (∀ p ∈ P, primary p ∧ Squarefree p ∧ norm p ≤ Y^(1+c/128)) →
      (∀ q ∈ Q, primary q ∧ norm q ≤ Y^(c/128)) →
      ∀ χ : Eisenstein → ℂ,
      (∀ b ∈ largePrimePowerSupport Y c, ‖χ b‖ ≤ 1) →
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primaryPrime, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.largePrimePowerSupport