AllShortMoments.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Uniform exceptional-moment savings when every actual short factor stays a fixed distance below length exponent one.

lemma OAI.CubicFirstMoment.short_length_le_scale line 12

theorem OAI.CubicFirstMoment.all_short_cubic_moment line 24

Source documentation

The all-short first exceptional configuration has a uniform power saving. The actual short arithmetic coefficients and independent bounded twists are allowed to vary freely; no amplitude or row-cardinality hypotheses remain.

theorem all_short_cubic_moment {δ C : ℝ} (hδ : 0 < δ) (hC : 0 < C) :
    ∃ ε : ℝ, 0 < ε ∧ ∃ Y₀ : ℝ, ∀ (F : ShortFactorFamily ι) (j : ℕ)
      (Y : ℝ) (S : Finset Eisenstein), Y₀ ≤ Y →
      (∀ i, F.length j i ≤ Y^(1-δ)) →
      (Y/C ≤ ∏ i, F.length j i) → (∏ i, F.length j i) ≤ C*Y →
      (∀ p ∈ S, gramDyad Y p) →
      (∑ p ∈ S, ‖∏ i, F.cubicValue j i p‖^2) ≤ Y^(7/3-ε) := by
…

Mentions: OAI.CubicFirstMoment.ShortFactorFamily, OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.gramDyad

theorem OAI.CubicFirstMoment.all_short_mixed_moment line 57

Source documentation

The all-short balanced exceptional configuration has the same uniform saving, using only the published additive large sieve as analytic input.

theorem all_short_mixed_moment (hHuxley : HuxleyAdditiveLargeSieve)
    {δ C : ℝ} (hδ : 0 < δ) (hC : 0 < C) :
    ∃ ε : ℝ, 0 < ε ∧ ∃ Y₀ : ℝ, ∀ (F : ShortFactorFamily ι) (j : ℕ)
      (Y : ℝ) (S : Finset (Eisenstein × Eisenstein)), Y₀ ≤ Y →
      (∀ i, F.length j i ≤ Y^(1-δ)) →
      (Y/C ≤ ∏ i, F.length j i) → (∏ i, F.length j i) ≤ C*Y →
      (∀ p ∈ S, PrimarySquarefreePair p ∧ norm p.1 ≤ Y^(1/3:ℝ) ∧
        norm p.2 ≤ Y^(1/3:ℝ)) →
      (∑ p ∈ S, ‖∏ i, F.mixedValue j i p‖^2) ≤ Y^(7/3-ε) := by
…

Mentions: OAI.CubicFirstMoment.HuxleyAdditiveLargeSieve, OAI.CubicFirstMoment.ShortFactorFamily, OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.PrimarySquarefreePair, OAI.CubicFirstMoment.norm

theorem OAI.CubicFirstMoment.large_cubic_moment_has_long_factor line 93

Source documentation

Any larger first-configuration moment forces a factor of almost full length. This is the finite alternative used in the dominant-factor case.

theorem large_cubic_moment_has_long_factor {δ C : ℝ} (hδ : 0 < δ) (hC : 0 < C) :
    ∃ ε : ℝ, 0 < ε ∧ ∃ Y₀ : ℝ, ∀ (F : ShortFactorFamily ι) (j : ℕ)
      (Y : ℝ) (S : Finset Eisenstein), Y₀ ≤ Y →
      (Y/C ≤ ∏ i, F.length j i) → (∏ i, F.length j i) ≤ C*Y →
      (∀ p ∈ S, gramDyad Y p) →
      Y^(7/3-ε) < (∑ p ∈ S, ‖∏ i, F.cubicValue j i p‖^2) →
      ∃ i, Y^(1-δ) < F.length j i := by
…

Mentions: OAI.CubicFirstMoment.ShortFactorFamily, OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.gramDyad

theorem OAI.CubicFirstMoment.large_mixed_moment_has_long_factor line 108

Source documentation

The analogous finite dominant-factor alternative for balanced rows.

theorem large_mixed_moment_has_long_factor (hHuxley : HuxleyAdditiveLargeSieve)
    {δ C : ℝ} (hδ : 0 < δ) (hC : 0 < C) :
    ∃ ε : ℝ, 0 < ε ∧ ∃ Y₀ : ℝ, ∀ (F : ShortFactorFamily ι) (j : ℕ)
      (Y : ℝ) (S : Finset (Eisenstein × Eisenstein)), Y₀ ≤ Y →
      (Y/C ≤ ∏ i, F.length j i) → (∏ i, F.length j i) ≤ C*Y →
      (∀ p ∈ S, PrimarySquarefreePair p ∧ norm p.1 ≤ Y^(1/3:ℝ) ∧
        norm p.2 ≤ Y^(1/3:ℝ)) →
      Y^(7/3-ε) < (∑ p ∈ S, ‖∏ i, F.mixedValue j i p‖^2) →
      ∃ i, Y^(1-δ) < F.length j i := by
…

Mentions: OAI.CubicFirstMoment.HuxleyAdditiveLargeSieve, OAI.CubicFirstMoment.ShortFactorFamily, OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.PrimarySquarefreePair, OAI.CubicFirstMoment.norm