OAI/NumberTheory/CubicMoment/Estimates/MomentExponents.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CubicFirstMoment.HasPowerExponent line 13
2. theorem OAI.CubicFirstMoment.HasPowerExponent.const line 16
3. theorem OAI.CubicFirstMoment.HasPowerExponent.mul line 20
4. theorem OAI.CubicFirstMoment.HasPowerExponent.rpow line 28
5. theorem OAI.CubicFirstMoment.HasPowerExponent.natPow line 35
6. lemma OAI.CubicFirstMoment.log_max_pos line 42
7. theorem OAI.CubicFirstMoment.HasPowerExponent.add line 48
8. theorem OAI.CubicFirstMoment.HasPowerExponent.mono line 75
9. lemma OAI.CubicFirstMoment.remove_positive_loss line 83
10. theorem OAI.CubicFirstMoment.cubic_moment_exponent line 96

    Source documentation

    Taking actual logarithmic limits of the sharp cubic moment gives the numerical inequality used in the first exceptional configuration.

    theorem cubic_moment_exponent {Y R V N L : ℕ → ℝ} {r v n z : ℝ}
        (hY : Tendsto Y atTop atTop)
        (hRp : ∀ᶠ j in atTop, 0 < R j) (hVp : ∀ᶠ j in atTop, 0 < V j)
        (hNp : ∀ᶠ j in atTop, 0 < N j) (hLp : ∀ᶠ j in atTop, 0 < L j)
        (hR : HasPowerExponent Y R r) (hV : HasPowerExponent Y V v)
        (hN : HasPowerExponent Y N n) (hL : HasPowerExponent Y L z)
        (hmoment : ∀ ε : ℝ, 0 < ε → ∃ C : ℝ, 0 < C ∧
          ∀ᶠ j in atTop, R j*(V j)^2 ≤
            C*(N j*L j)^ε*L j*(N j+L j+(N j*L j)^(2/3:ℝ))) :
        r+2*v ≤ z+max (max n z) ((2/3:ℝ)*(n+z)) := by
    …

    Mentions: OAI.CubicFirstMoment.HasPowerExponent

11. theorem OAI.CubicFirstMoment.ordinary_moment_exponent line 131

    Source documentation

    The ordinary mixed-character moment gives the second configuration's limiting exponent, again by taking limits of actual inequalities.

    theorem ordinary_moment_exponent {Y R V Q L : ℕ → ℝ} {r v q z : ℝ}
        (hY : Tendsto Y atTop atTop)
        (hRp : ∀ᶠ j in atTop, 0 < R j) (hVp : ∀ᶠ j in atTop, 0 < V j)
        (hQp : ∀ᶠ j in atTop, 0 < Q j) (hLp : ∀ᶠ j in atTop, 0 < L j)
        (hR : HasPowerExponent Y R r) (hV : HasPowerExponent Y V v)
        (hQ : HasPowerExponent Y Q q) (hL : HasPowerExponent Y L z)
        (hmoment : ∀ ε : ℝ, 0 < ε → ∃ C : ℝ, 0 < C ∧
          ∀ᶠ j in atTop, R j*(V j)^2 ≤ C*(Q j*L j)^ε*L j*((Q j)^2+L j)) :
        r+2*v ≤ z+max (2*q) z := by
    …

    Mentions: OAI.CubicFirstMoment.HasPowerExponent