OAI/NumberTheory/CubicMoment/Estimates/ShortFactorGram.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Repeated short factors in the final Gram estimate.

  1. def OAI.CubicFirstMoment.shortRepeatedSupport line 13
  2. def OAI.CubicFirstMoment.shortRepeatedCoefficient line 16
  3. lemma OAI.CubicFirstMoment.shortRepeatedSupport_mem line 21
  4. lemma OAI.CubicFirstMoment.shortRepeated_polynomial line 32
  5. theorem OAI.CubicFirstMoment.shortRepeated_energy line 43

    Source documentation

    The actual coefficient energy has only an arbitrarily small power loss; all logarithmic weights and repeated factorizations are included.

    theorem shortRepeated_energy (m : ℕ) {ε : ℝ} (hε : 0 < ε) :
    ∃ C : ℝ, 0 < C ∧ ∀ (F X : ℝ) (A : EisensteinArithmeticFunction)
      (u : Eisenstein → ℂ), ShortArithmeticFactor F A → 1 ≤ X →
      (∀ n ∈ primaryElementBall X, ‖u n‖ ≤ 1) →
      (∑ b ∈ shortRepeatedSupport m X, ‖shortRepeatedCoefficient m X A u b‖^2) ≤
        C*(X^m)^(1+ε) := by
…

    Mentions: OAI.CubicFirstMoment.EisensteinArithmeticFunction, OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.ShortArithmeticFactor, OAI.CubicFirstMoment.primaryElementBall, OAI.CubicFirstMoment.shortRepeatedSupport, OAI.CubicFirstMoment.shortRepeatedCoefficient

  6. theorem OAI.CubicFirstMoment.shortRepeated_gram_large_values line 101

    Source documentation

    Applying the proved Gram theorem to the literal copied factor gives an exact finite large-value inequality with its true coefficient energy.

    theorem shortRepeated_gram_large_values (m : ℕ) {ε : ℝ} (hε : 0 < ε) :
    ∃ C D E : ℝ, 0 < C ∧ 0 < D ∧ 0 < E ∧
      ∀ (F X P V : ℝ) (A : EisensteinArithmeticFunction) (u : Eisenstein → ℂ)
        (Q : Finset Eisenstein), ShortArithmeticFactor F A → 1 ≤ X → 1 ≤ P → 0 < V →
        (∀ n ∈ primaryElementBall X, ‖u n‖ ≤ 1) →
        (∀ p ∈ Q, gramDyad P p) →
        (∀ p ∈ Q, V ≤ ‖primaryIdealPolynomial X A
          (fun n => u n*cubicSymbol p n)‖^m) →
        (Q.card:ℝ)*V^4 ≤ 2*(E*(X^m)^(1+ε))*(D*(X^m))*V^2+
          (E*(X^m)^(1+ε))^2*
            (C*(P*(X^m))^ε*(X^m)*(P+(P^3/(X^m))^(2/3:ℝ))) := by
…

    Mentions: OAI.CubicFirstMoment.EisensteinArithmeticFunction, OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.ShortArithmeticFactor, OAI.CubicFirstMoment.primaryElementBall, OAI.CubicFirstMoment.gramDyad, OAI.CubicFirstMoment.primaryIdealPolynomial, OAI.CubicFirstMoment.cubicSymbol

  7. lemma OAI.CubicFirstMoment.HasPowerExponent.const_mul line 124
  8. lemma OAI.CubicFirstMoment.HasPowerExponent.div line 131
  9. lemma OAI.CubicFirstMoment.remove_gram_loss line 139
  10. theorem OAI.CubicFirstMoment.gram_large_values_exponent line 152

    Source documentation

    The root-free Gram inequality has a strict limiting exponent gap. This takes limits of the actual finite inequality, including the energy loss.

    theorem gram_large_values_exponent {Y R V N L : ℕ → ℝ} {r v z : ℝ}
    (hY : Tendsto Y atTop atTop) (hz : 0 ≤ z)
    (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 1) (hL : HasPowerExponent Y L z)
    (hgram : ∀ ε : ℝ, 0 < ε → ∃ A B : ℝ, 0 < A ∧ 0 < B ∧
      ∀ᶠ j in atTop, R j*(V j)^4 ≤
        A*(L j)^(2+ε)*(V j)^2+
        B*(L j)^(3+2*ε)*(N j*L j)^ε*
          (N j+((N j)^3/L j)^(2/3:ℝ))) :
    r+4*v ≤ max (2*z+2*v) (3*z+max 1 (2-2*z/3)) := by
…

    Mentions: OAI.CubicFirstMoment.HasPowerExponent

  11. lemma OAI.CubicFirstMoment.gram_energy_group line 211
  12. theorem OAI.CubicFirstMoment.ShortFactorFamily.copied_rows_gram_exponent line 231

    Source documentation

    A fixed number of copies of an actual short factor satisfies the limiting Gram inequality; no coefficient-energy exponent is assumed.

    theorem ShortFactorFamily.copied_rows_gram_exponent {ι : Type*}
    (F : ShortFactorFamily ι) (i : ι) (m : ℕ)
    {Y N : ℕ → ℝ} (P : ℕ → Finset Eisenstein) (B : ℕ → ℝ)
    {r a v : ℝ} (hY : Tendsto Y atTop atTop) (hN : ∀ j, 1 ≤ N j)
    (hP : ∀ j, ∀ p ∈ P j, gramDyad (N j) p)
    (hPne : ∀ j, (P j).Nonempty) (hB : ∀ j, 0 < B j)
    (hrow : ∀ j, ∀ p ∈ P j, B j ≤ ‖F.cubicValue j i p‖)
    (hRexp : HasPowerExponent Y (fun j => ((P j).card:ℝ)) r)
    (hNexp : HasPowerExponent Y N 1)
    (hXexp : HasPowerExponent Y (fun j => F.length j i) a)
    (hBexp : HasPowerExponent Y B v) :
    r+4*((m:ℝ)*v) ≤ max (2*((m:ℝ)*a)+2*((m:ℝ)*v))
…

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

  13. theorem OAI.CubicFirstMoment.ShortFactorFamily.copied_rows_gram_contradiction line 264

    Source documentation

    The saturated first configuration cannot contain a positive short factor with a fixed number of copies in the interior Gram range.

    theorem ShortFactorFamily.copied_rows_gram_contradiction {ι : Type*}
    (F : ShortFactorFamily ι) (i : ι) (m : ℕ)
    {Y N : ℕ → ℝ} (P : ℕ → Finset Eisenstein) (B : ℕ → ℝ)
    {a : ℝ} (hY : Tendsto Y atTop atTop) (hN : ∀ j, 1 ≤ N j)
    (hP : ∀ j, ∀ p ∈ P j, gramDyad (N j) p)
    (hPne : ∀ j, (P j).Nonempty) (hB : ∀ j, 0 < B j)
    (hrow : ∀ j, ∀ p ∈ P j, B j ≤ ‖F.cubicValue j i p‖)
    (hRexp : HasPowerExponent Y (fun j => ((P j).card:ℝ)) (2/3))
    (hNexp : HasPowerExponent Y N 1)
    (hXexp : HasPowerExponent Y (fun j => F.length j i) a)
    (hBexp : HasPowerExponent Y B (5*a/6))
    (hz₀ : 4/3 < (m:ℝ)*a) (hz₁ : (m:ℝ)*a < 2) : False := by
…

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

  14. lemma OAI.CubicFirstMoment.exists_positive_short_factor line 296
  15. theorem OAI.CubicFirstMoment.ShortFactorFamily.first_rows_contradiction line 317

    Source documentation

    The complete short-factor contradiction in the first exceptional configuration. Both the rigidity and the final Gram bound apply to the literal polynomials defined by the given arithmetic family.

    theorem ShortFactorFamily.first_rows_contradiction {ι : Type*} [Fintype ι] [DecidableEq ι]
    (F : ShortFactorFamily ι) {Y N : ℕ → ℝ}
    (P : ℕ → Finset Eisenstein) (B : ℕ → ι → ℝ) {a v : ι → ℝ} {r : ℝ}
    (hY : Tendsto Y atTop atTop) (hN : ∀ j, 1 ≤ N j)
    (hP : ∀ j, ∀ p ∈ P j, gramDyad (N j) p)
    (hPne : ∀ j, (P j).Nonempty) (hB : ∀ j i, 0 < B j i)
    (hrow : ∀ j, ∀ p ∈ P j, ∀ i, B j i ≤ ‖F.cubicValue j i p‖)
    (hRexp : HasPowerExponent Y (fun j => ((P j).card:ℝ)) r)
    (hNexp : HasPowerExponent Y N 1)
    (hXexp : ∀ i, HasPowerExponent Y (fun j => F.length j i) (a i))
    (hBexp : ∀ i, HasPowerExponent Y (fun j => B j i) (v i))
    (ha : ∀ i, a i < 1) (hsum : ∑ i, a i = 1)
…

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