OAI/NumberTheory/Ostmann/Characters/BonamiMonomialFamily.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.monomialCoefficients line 11
2. theorem OAI.Ostmann.monomialCoefficients_apply line 15
3. theorem OAI.Ostmann.monomialCoefficients_sum line 27
4. theorem OAI.Ostmann.monomialCoefficients_energy line 37
5. theorem OAI.Ostmann.bonami_monomial_family line 55

   Source documentation

   Apply the published cube bound after inserting the coefficient array by zero outside the actual monomial family.

   theorem bonami_monomial_family (hB : PublishedBonamiBound)
       {ι : Type*} [Fintype ι] (P : Finset ℕ)
       (σ : ι → Finset P) (hσ : Function.Injective σ) (a : ι → ℝ)
       (l : ℕ) (hl : 0 < l) :
       (Fintype.card (P → Bool) : ℝ)⁻¹ *
         ∑ ε : P → Bool, |∑ i, a i * rademacherMonomial (σ i) ε| ^ (2 * l) ≤
         (∑ i, ((2 * l - 1 : ℕ) : ℝ) ^ (σ i).card * (a i) ^ 2) ^ l := by
   …

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