OAI/NumberTheory/Ostmann/Characters/BonamiTensor.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Tensorizing the two-point Bonami estimate on a finite cube

  1. def OAI.Ostmann.booleanMoment line 14
  2. theorem OAI.Ostmann.booleanMoment_reindex line 18
  3. theorem OAI.Ostmann.booleanMoment_option line 29
  4. theorem OAI.Ostmann.booleanPolynomial_moment line 48

    Source documentation

    The exact weighted even-moment bound for arbitrary finite Boolean cubes.

    theorem booleanPolynomial_moment (l : ℕ) (hl : 0 < l)
    (α : Type u) [Fintype α] (a : (α → Bool) → ℝ) :
    booleanMoment l a ≤ (Fintype.card (α → Bool) : ℝ) *
      booleanEnergy ((2 * l - 1 : ℕ) : ℝ) a ^ l := by
…

    Mentions: OAI.Ostmann.booleanMoment, OAI.Ostmann.booleanEnergy