OAI/Combinatorics/SharpThreshold/FourierHypercontractive.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem313.BiasedFourier.scalar_synthesis_fourth line 19

   Source documentation

   The scalar hypercontractive estimate in normalized character notation.

   theorem scalar_synthesis_fourth {p : ℝ} (hp : 0 < p) (hp1 : p < 1)
       (a b : ℝ) :
       (1 - p) * (a + (Real.sqrt (p * (1-p)) / 4) * chi p false * b) ^ 4 +
         p * (a + (Real.sqrt (p * (1-p)) / 4) * chi p true * b) ^ 4 ≤
         (a ^ 2 + b ^ 2) ^ 2 := by
   …

   Mentions: OAI.Problem313.BiasedFourier.chi

2. theorem OAI.Problem313.BiasedFourier.synthesis_fourth_option_of_split line 36

   Source documentation

   Tensorization step for an additional Boolean coordinate, in spectral form.

   theorem synthesis_fourth_option_of_split {ι : Type u} [Fintype ι]
       {p : ℝ} (hp : 0 < p) (hp1 : p < 1)
       (hsplit : ∀ g : (Option ι → Bool) → ℝ,
         (∑ x, weight p x * g x) =
           (1-p) * (∑ y : ι → Bool, weight p y * g (fun t => Option.elim t false y)) +
           p * (∑ y : ι → Bool, weight p y * g (fun t => Option.elim t true y)))
       (ih : ∀ c : Finset ι → ℝ,
         (∑ x, weight p x * (∑ S, (Real.sqrt (p*(1-p))/4) ^ S.card *
           c S * char p S x) ^ 4) ≤ (∑ S, c S ^ 2) ^ 2)
       (c : Finset (Option ι) → ℝ) :
       (∑ x, weight p x * (∑ S, (Real.sqrt (p*(1-p))/4) ^ S.card *
         c S * char p S x) ^ 4) ≤ (∑ S, c S ^ 2) ^ 2 := by
   …

   Mentions: OAI.Problem313.BiasedFourier.weight, OAI.Problem313.BiasedFourier.char

3. theorem OAI.Problem313.BiasedFourier.synthesis_fourth_empty line 86

   Source documentation

   Initial case of the finite-coordinate tensorization induction.

   theorem synthesis_fourth_empty {ι : Type u} [Fintype ι] [IsEmpty ι]
       (p : ℝ) (c : Finset ι → ℝ) :
       (∑ x : ι → Bool, weight p x *
         (∑ S, (Real.sqrt (p*(1-p))/4) ^ S.card * c S * char p S x) ^ 4) ≤
         (∑ S, c S ^ 2) ^ 2 := by
   …

   Mentions: OAI.Problem313.BiasedFourier.weight, OAI.Problem313.BiasedFourier.char

4. theorem OAI.Problem313.BiasedFourier.synthesis_fourth_bound line 97

   Source documentation

   Biased product hypercontractivity in its root-free, arbitrary-coefficient form.

   theorem synthesis_fourth_bound {ι : Type u} [Fintype ι]
       {p : ℝ} (hp : 0 < p) (hp1 : p < 1) (c : Finset ι → ℝ) :
       (∑ x, weight p x * (∑ S, (Real.sqrt (p*(1-p))/4) ^ S.card *
         c S * char p S x) ^ 4) ≤ (∑ S, c S ^ 2) ^ 2 := by
   …

   Mentions: OAI.Problem313.BiasedFourier.weight, OAI.Problem313.BiasedFourier.char

5. theorem OAI.Problem313.BiasedFourier.noise_fourth_bound line 117

   Source documentation

   The noise operator contracts the weighted second moment into the fourth moment.

   theorem noise_fourth_bound {ι : Type u} [Fintype ι]
       {p : ℝ} (hp : 0 < p) (hp1 : p < 1) (g : (ι → Bool) → ℝ) :
       (∑ x, weight p x * (∑ S, (Real.sqrt (p*(1-p))/4) ^ S.card *
         coeff p g S * char p S x) ^ 4) ≤ (∑ x, weight p x * (g x) ^ 2) ^ 2 := by
   …

   Mentions: OAI.Problem313.BiasedFourier.weight, OAI.Problem313.BiasedFourier.coeff, OAI.Problem313.BiasedFourier.char