CubicMomentGram.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The Gram estimate for a finite cubic-character moment

This supplies the near-orthogonality inequality in the exceptional-character-moment argument for the actual character polynomials. The only analytic estimate used here is the cubic Gram theorem.

def OAI.CubicFirstMoment.primarySieveWeight line 21
lemma OAI.CubicFirstMoment.primarySieveWeight_nonneg line 24
lemma OAI.CubicFirstMoment.cutoff_gram_finite line 31
lemma OAI.CubicFirstMoment.cutoff_gram_diagonal_le line 52
lemma OAI.CubicFirstMoment.cutoff_gram_row_le line 81

theorem OAI.CubicFirstMoment.cubic_moment_gram_bound line 116

Source documentation

A concrete smooth majorant converts the proved Gram theorem into a bound for any finite primary-supported cubic-character polynomial.

theorem cubic_moment_gram_bound {ε : ℝ} (hε : 0 < ε) :
    ∃ C D : ℝ, 0 < C ∧ 0 < D ∧
      ∀ (Q N : Finset Eisenstein) (P Z : ℝ) (v : Eisenstein → ℂ),
      1 ≤ P → 1 ≤ Z → (∀ p ∈ Q, gramDyad P p) →
      (∀ n ∈ N, primary n ∧ norm n ≤ Z) →
      (∑ p ∈ Q, ‖∑ n ∈ N, v n*cubicSymbol p n‖^2) ≤
        (D*Z + Real.sqrt ((Q.card : ℝ)*
          (C*(P*Z)^ε*Z*(P+(P^3/Z)^(2/3 : ℝ))))) * ∑ n ∈ N, ‖v n‖^2 := by
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.gramDyad, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.cubicSymbol