WeightedSmoothCharacterMean.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Weighted smooth character means at the actual truncation cutoff

theorem OAI.Ostmann.weighted_smooth_character_error line 12

Source documentation

A finite coefficient bound costs no factor equal to the number of characters.

theorem weighted_smooth_character_error (F : Finset PrimitiveComplexCharacter)
    (c : PrimitiveComplexCharacter → ℂ) (c₀ : ℂ) (B X : ℝ)
    (hc₀ : ‖c₀‖ ≤ B) (hc : ∀ χ ∈ F, ‖c χ‖ ≤ B) :
    ‖c₀ * smoothMangoldtMean 1 1 X +
        ∑ χ ∈ F, c χ * smoothMangoldtMean χ.modulus χ.character X -
        c₀ * smoothPrincipalMain X‖ ≤
      B * (smoothPrincipalError X +
        ∑ χ ∈ F, ‖smoothMangoldtMean χ.modulus χ.character X‖) := by
…

Mentions: OAI.Ostmann.PrimitiveComplexCharacter, OAI.Ostmann.smoothMangoldtMean, OAI.Ostmann.smoothPrincipalMain, OAI.Ostmann.smoothPrincipalError

theorem OAI.Ostmann.weighted_sparse_character_decay line 37