SharpPrimaryMoments.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The sharp bounded-coefficient cubic sieve, specialized to actual primary convolutions. The pointwise divisor bound is essential here.

lemma OAI.CubicFirstMoment.finite_polynomial_dyad_partition line 14

theorem OAI.CubicFirstMoment.bounded_cubic_moment line 38

Source documentation

Sharp cutoff form of the proved bounded-coefficient inner extension. The coefficient support may contain cubes and need not be squarefree.

theorem bounded_cubic_moment {ε : ℝ} (hε : 0 < ε) :
    ∃ C : ℝ, 0 < C ∧ ∀ (P H : Finset Eisenstein) (N Y D : ℝ),
      1 ≤ N → 1 ≤ Y → 0 ≤ D →
      (∀ a ∈ P, primary a ∧ Squarefree a ∧ norm a ≤ N) →
      (∀ n ∈ H, n ≠ 0 ∧ norm n ≤ Y) → ∀ v : Eisenstein → ℂ,
      (∀ n ∈ H, ‖v n‖ ≤ D) →
      (∑ a ∈ P, ‖∑ n ∈ H, v n*cubicSymbol a n‖^2) ≤
        C*(N*Y)^ε*Y*(N+Y+(N*Y)^(2/3:ℝ))*D^2 := by
…

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

theorem OAI.CubicFirstMoment.primary_orderedConvolution_norm line 110

Source documentation

Pointwise coefficient bound for the actual independent primary convolution, uniform in its supports and independent factor weights.

theorem primary_orderedConvolution_norm {δ : ℝ} (hδ : 0 < δ) :
    ∃ C : ℝ, 0 < C ∧ ∀ (S : ι → Finset Eisenstein)
      (w : ι → Eisenstein → ℂ) (M : ι → ℝ),
      (∀ i, ∀ a ∈ S i, primary a) → (∀ 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.primary, OAI.CubicFirstMoment.orderedConvolutionSupport, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.orderedConvolution

theorem OAI.CubicFirstMoment.primaryConvolution_sharp_twisted_moment line 136

Source documentation

Sharp cubic moment for the actual collected primary convolution, including any fixed coefficient twist of norm at most one.

theorem primaryConvolution_sharp_twisted_moment {ε δ : ℝ}
    (hε : 0 < ε) (hδ : 0 < δ) :
    ∃ C : ℝ, 0 < C ∧ ∀ (S : ι → Finset Eisenstein)
      (w : ι → Eisenstein → ℂ) (M : ι → ℝ),
      (∀ i, ∀ a ∈ S i, primary a) → (∀ i, 0 ≤ M i) →
      (∀ i, ∀ a ∈ S i, ‖w i a‖ ≤ M i) →
      ∀ (P : Finset Eisenstein) (N Y : ℝ), 1 ≤ N → 1 ≤ Y →
      (∀ a ∈ P, primary a ∧ Squarefree a ∧ norm a ≤ N) →
      (∀ f ∈ Fintype.piFinset S, norm (∏ i, f i) ≤ Y) →
      ∀ χ : Eisenstein → ℂ, (∀ b ∈ orderedConvolutionSupport S, ‖χ b‖ ≤ 1) →
      (∑ a ∈ P, ‖∑ b ∈ orderedConvolutionSupport S,
        (orderedConvolution S w b*χ b)*cubicSymbol a b‖^2) ≤
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.orderedConvolutionSupport, OAI.CubicFirstMoment.orderedConvolution, OAI.CubicFirstMoment.cubicSymbol

theorem OAI.CubicFirstMoment.primaryConvolution_sharp_product_moment line 174

Source documentation

The untwisted product polynomial has the same sharp moment; every factor is permitted to be an arbitrary primary-element polynomial.

theorem primaryConvolution_sharp_product_moment {ε δ : ℝ}
    (hε : 0 < ε) (hδ : 0 < δ) :
    ∃ C : ℝ, 0 < C ∧ ∀ (S : ι → Finset Eisenstein)
      (w : ι → Eisenstein → ℂ) (M : ι → ℝ),
      (∀ i, ∀ a ∈ S i, primary a) → (∀ i, 0 ≤ M i) →
      (∀ i, ∀ a ∈ S i, ‖w i a‖ ≤ M i) →
      ∀ (P : Finset Eisenstein) (N Y : ℝ), 1 ≤ N → 1 ≤ Y →
      (∀ a ∈ P, primary a ∧ Squarefree a ∧ norm a ≤ N) →
      (∀ f ∈ Fintype.piFinset S, norm (∏ i, f i) ≤ Y) →
      (∑ a ∈ P, ‖primeCubicProductPolynomial S w a‖^2) ≤
        C*(N*Y)^ε*Y*(N+Y+(N*Y)^(2/3:ℝ))*(Y^δ*(∏ i, M i)^2) := by
…

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