FirstShapeErrorMoment.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Sparse error terms in the first exceptional conductor configuration.

theorem OAI.CubicFirstMoment.unrestricted_mixed_product_sieve line 14
lemma OAI.CubicFirstMoment.first_shape_sieve_power line 51

theorem OAI.CubicFirstMoment.first_shape_sparse_mixed_moment line 95

Source documentation

Sparse coefficient energy supplies a fixed saving for the first exceptional conductor shape. All arithmetic support conditions are kept on the actual coefficient and character sets.

theorem first_shape_sparse_mixed_moment {θ : ℝ} (hθ : 0 < θ) (hθ₁ : θ ≤ 1) :
    ∃ C : ℝ, 0 < C ∧ ∀ (Y E : ℝ), 1 ≤ Y → 0 ≤ E →
      ∀ (P Q H : Finset Eisenstein),
      (∀ p ∈ P, primary p ∧ Squarefree p ∧ norm p ≤ Y^(1+θ/16)) →
      (∀ q ∈ Q, primary q ∧ norm q ≤ Y^(θ/16)) →
      (∀ h ∈ H, h ≠ 0 ∧ norm h ≤ Y) →
      ∀ v : Eisenstein → ℂ, (∑ h ∈ H, ‖v h‖^2) ≤ E*Y^(1-θ) →
      (∑ q ∈ Q, ∑ p ∈ P, ‖∑ h ∈ H, v h*mixedCubic p q h‖^2) ≤
        C*E*Y^(7/3-θ/2) := by
…

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

theorem OAI.CubicFirstMoment.repeatedPrime_first_shape_second_moment line 129

Source documentation

The prime-to-squarefree discrepancy satisfies the first exceptional second-moment bound, with all fixed angular and norm twists retained.

theorem repeatedPrime_first_shape_second_moment
    {ι : Type*} [Fintype ι] [DecidableEq ι] {c : ℝ}
    (hc : 0 < c) (hc₁ : c ≤ 1) :
    ∃ C : ℝ, 0 < C ∧ ∀ (S : ι → Finset Eisenstein)
      (w : ι → Eisenstein → ℂ) (M : ι → ℝ) (Y : ℝ),
      1 ≤ Y → (∀ i, 0 ≤ M i) →
      (∀ i, ∀ p ∈ S i, primaryPrime p ∧ Y^c < norm p) →
      (∀ f ∈ Fintype.piFinset S, norm (∏ i, f i) ≤ Y) →
      (∀ i, ∀ p ∈ S i, ‖w i p‖ ≤ M i) →
      ∀ P Q : Finset Eisenstein,
      (∀ p ∈ P, primary p ∧ Squarefree p ∧ norm p ≤ Y^(1+c/32)) →
      (∀ q ∈ Q, primary q ∧ norm q ≤ Y^(c/32)) →
…

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

theorem OAI.CubicFirstMoment.primePower_first_shape_second_moment line 175

Source documentation

Higher prime powers, including powers of small primes, have a sparse enough actual support for the same first-shape argument.

theorem primePower_first_shape_second_moment {c : ℝ} (hc : 0 < c) (hc₁ : c ≤ 1) :
    ∃ C : ℝ, 0 < C ∧ ∀ (Y A : ℝ), 1 ≤ Y → 0 ≤ A →
      ∀ 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)) →
      ∀ v : Eisenstein → ℂ, (∀ b ∈ largePrimePowerSupport Y c, ‖v b‖ ≤ A) →
      (∑ q ∈ Q, ∑ p ∈ P, ‖∑ b ∈ largePrimePowerSupport Y c,
        v b*mixedCubic p q b‖^2) ≤ C*A^2*Y^(7/3-c/16) := by
…

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