OAI/NumberTheory/CubicMoment/Estimates/ShortFactorUniform.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.CubicFirstMoment.power_saving_of_no_countersequence line 12
2. lemma OAI.CubicFirstMoment.countersequence_tendsto line 28
3. lemma OAI.CubicFirstMoment.countersequence_lower_exponent line 33
4. lemma OAI.CubicFirstMoment.countersequence_lower_ge_one line 40
5. lemma OAI.CubicFirstMoment.HasPowerExponent.of_comparable line 48

   Source documentation

   Multiplicative comparability is enough to identify the total logarithmic length exponent; the bounded dyadic discrepancy disappears in the limit.

   lemma HasPowerExponent.of_comparable {Y f : ℕ → ℝ} {C : ℝ}
       (hY : Tendsto Y atTop atTop) (hC : 0 < C)
       (hbound : ∀ᶠ j in atTop, Y j/C ≤ f j ∧ f j ≤ C*Y j) :
       HasPowerExponent Y f 1 := by
   …

   Mentions: OAI.CubicFirstMoment.HasPowerExponent

6. structure OAI.CubicFirstMoment.ShortMomentInstance line 66
7. def OAI.CubicFirstMoment.assembleShortFamily line 71
8. def OAI.CubicFirstMoment.cubicInstanceMoment line 83
9. def OAI.CubicFirstMoment.cubicInstanceAdmissible line 86
10. theorem OAI.CubicFirstMoment.cubic_short_uniform_power line 96

    Source documentation

    Uniform power saving for all actual first-configuration short factors separated from length exponent one. The auxiliary size bounds are explicit.

    theorem cubic_short_uniform_power {δ H D C : ℝ}
        (hδ : 0 < δ) (hH : 0 ≤ H) (hD : 0 ≤ D) (hC : 0 < C) :
        ∃ ε : ℝ, 0 < ε ∧ ∃ Y₀ : ℝ,
          ∀ x : ShortMomentInstance ι Eisenstein, cubicInstanceAdmissible δ H D C x →
            Y₀ ≤ x.scale → cubicInstanceMoment x ≤ x.scale^(7/3-ε) := by
    …

    Mentions: OAI.CubicFirstMoment.ShortMomentInstance, OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.cubicInstanceAdmissible, OAI.CubicFirstMoment.cubicInstanceMoment

11. def OAI.CubicFirstMoment.mixedInstanceMoment line 116
12. def OAI.CubicFirstMoment.mixedInstanceAdmissible line 119
13. theorem OAI.CubicFirstMoment.mixed_short_uniform_power line 130

    Source documentation

    The analogous uniform power saving in the balanced configuration.

    theorem mixed_short_uniform_power (hHuxley : HuxleyAdditiveLargeSieve) {δ H D C : ℝ}
        (hδ : 0 < δ) (hH : 0 ≤ H) (hD : 0 ≤ D) (hC : 0 < C) :
        ∃ ε : ℝ, 0 < ε ∧ ∃ Y₀ : ℝ,
          ∀ x : ShortMomentInstance ι (Eisenstein × Eisenstein),
            mixedInstanceAdmissible δ H D C x → Y₀ ≤ x.scale →
              mixedInstanceMoment x ≤ x.scale^(7/3-ε) := by
    …

    Mentions: OAI.CubicFirstMoment.HuxleyAdditiveLargeSieve, OAI.CubicFirstMoment.ShortMomentInstance, OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.mixedInstanceAdmissible, OAI.CubicFirstMoment.mixedInstanceMoment