WeightedGram.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

A smooth majorant in the Gram bound

The majorant needs to be at least one only on the coefficient support. It may vanish elsewhere. This is the weighted Cauchy step used to pass from smooth character Gram estimates to finite Dirichlet polynomials.

def OAI.CubicFirstMoment.weightedFiniteGram line 18
theorem OAI.CubicFirstMoment.weightedFiniteGram_eq line 22

theorem OAI.CubicFirstMoment.weighted_gram_operator_le line 39

Source documentation

The Gram row bound controls coefficients beneath any nonnegative smooth majorant which is at least one on their support.

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

Mentions: OAI.CubicFirstMoment.weightedFiniteGram