GramLargeValues.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Large values from the cubic Gram bound

Eliminating the row count from the square root preserves the saving in the near-orthogonality argument. No large-value estimate is assumed.

lemma OAI.CubicFirstMoment.gram_scalar_large_values line 16

theorem OAI.CubicFirstMoment.cubic_gram_large_value_count line 41

Source documentation

All rows exceeding L force an explicit cardinality bound. This is the finite large-value inequality needed before taking exponents.

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

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