OAI/NumberTheory/Ostmann/Characters/SquarefreeBonami.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.primeFactorSubset line 12
2. theorem OAI.Ostmann.mem_primeFactorSubset line 15
3. theorem OAI.Ostmann.primeFactorSubset_map line 19
4. theorem OAI.Ostmann.primeFactorSubset_card line 29
5. theorem OAI.Ostmann.primeFactorSubset_injective line 33
6. theorem OAI.Ostmann.bonami_squarefree_family line 47

   Source documentation

   This is the even moment bound in the manuscript, indexed by the squarefree integers themselves.

   theorem bonami_squarefree_family (hB : PublishedBonamiBound) (P S : Finset ℕ)
       (hS : ∀ s ∈ S, Squarefree s) (hP : ∀ s ∈ S, s.primeFactors ⊆ P)
       (a : S → ℝ) (l : ℕ) (hl : 0 < l) :
       (Fintype.card (P → Bool) : ℝ)⁻¹ *
         ∑ ε : P → Bool,
           |∑ s : S, a s * rademacherMonomial (primeFactorSubset P s.val) ε| ^ (2 * l) ≤
         (∑ s : S, ((2 * l - 1 : ℕ) : ℝ) ^ s.val.primeFactors.card * (a s) ^ 2) ^ l := by
   …

   Mentions: OAI.Ostmann.PublishedBonamiBound, OAI.Ostmann.rademacherMonomial, OAI.Ostmann.primeFactorSubset