OAI/NumberTheory/Ostmann/Characters/BonamiTwoPoint.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The elementary two-point estimate for the required Bonami bound

  1. theorem OAI.Ostmann.bonami_choose_bound line 13
  2. theorem OAI.Ostmann.sum_range_double line 50
  3. theorem OAI.Ostmann.even_power_binomial line 59
  4. theorem OAI.Ostmann.bonami_two_point line 96

    Source documentation

    Bonami's required even-moment inequality on one Boolean coordinate.

    theorem bonami_two_point (x y : ℝ) (l : ℕ) (hl : 0 < l) :
    (|x + y| ^ (2 * l) + |x - y| ^ (2 * l)) / 2 ≤
      (x ^ 2 + (2 * l - 1 : ℕ) * y ^ 2) ^ l := by
…