OAI/NumberTheory/CubicMoment/Estimates/GramOperator.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

From Gram row sums to character-polynomial bounds

Finite duality turns the row-sum bound into an operator estimate. This is the Cauchy/Gram step used after the multiplicity argument in the exceptional-character-moment argument.

  1. def OAI.CubicFirstMoment.finiteGram line 17
  2. lemma OAI.CubicFirstMoment.complex_sum_norm_sq_expansion line 20
  3. lemma OAI.CubicFirstMoment.finiteGram_star line 26
  4. lemma OAI.CubicFirstMoment.finite_gram_identity line 30
  5. theorem OAI.CubicFirstMoment.finite_gram_energy_le line 50
  6. theorem OAI.CubicFirstMoment.finite_gram_operator_le line 63

    Source documentation

    Duality exchanges rows and columns without loss.

    theorem finite_gram_operator_le {ι κ : Type*} (P : Finset ι) (N : Finset κ)
    (v : κ → ℂ) (T : ι → κ → ℂ) {R : ℝ} (hR : 0 ≤ R)
    (hrow : ∀ p ∈ P, ∑ q ∈ P, ‖finiteGram N T p q‖ ≤ R) :
    (∑ p ∈ P, ‖∑ n ∈ N, v n * T p n‖^2) ≤ R * ∑ n ∈ N, ‖v n‖^2 := by
…

    Mentions: OAI.CubicFirstMoment.finiteGram