OAI/Combinatorics/SharpThreshold/LowDegree.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem313.BiasedFourier.low_degree_estimate_of_noise line 21

   Source documentation

   The biased low-degree influence estimate, with the product noise contraction as its only remaining analytic premise.

   theorem low_degree_estimate_of_noise {p : ℝ} (hp : 0 < p) (hp1 : p < 1)
       (f : (ι → Bool) → Bool) (m : ℝ) (hm : 1 ≤ m)
       (horbit : ∀ i, Reindex.influence p f i ≤ (∑ j, Reindex.influence p f j) / m)
       (hnoise : ∀ a : Finset ι → ℝ,
         (∑ x, weight p x *
           (∑ S, (Real.sqrt (p * (1 - p)) / 4) ^ S.card * a S * char p S x) ^ 4) ≤
             (∑ S, (a S) ^ 2) ^ 2) :
       (∑ S : Finset ι,
         if S.Nonempty ∧ (S.card : ℝ) ≤ Real.sqrt (p * (1 - p)) * Real.log m / 64
         then coeff p (fun x => boolReal (f x)) S ^ 2 else 0) ≤
           m ^ (-1 / 4 : ℝ) * ∑ i, Reindex.influence p f i := by
   …

   Mentions: OAI.Problem313.Reindex.influence, OAI.Problem313.BiasedFourier.weight, OAI.Problem313.BiasedFourier.char, OAI.Problem313.BiasedFourier.coeff, OAI.Problem313.boolReal

2. theorem OAI.Problem313.BiasedFourier.low_degree_estimate_filter_of_noise line 65

   Source documentation

   Version of the low-degree estimate written as a filtered sum with the literal positive integer degree condition.

   theorem low_degree_estimate_filter_of_noise {p : ℝ} (hp : 0 < p) (hp1 : p < 1)
       (f : (ι → Bool) → Bool) (m : ℝ) (hm : 1 ≤ m)
       (horbit : ∀ i, Reindex.influence p f i ≤ (∑ j, Reindex.influence p f j) / m)
       (hnoise : ∀ a : Finset ι → ℝ,
         (∑ x, weight p x *
           (∑ S, (Real.sqrt (p * (1 - p)) / 4) ^ S.card * a S * char p S x) ^ 4) ≤
             (∑ S, (a S) ^ 2) ^ 2) :
       (∑ S ∈ (Finset.univ.filter fun S : Finset ι =>
         1 ≤ S.card ∧ (S.card : ℝ) ≤ Real.sqrt (p * (1 - p)) * Real.log m / 64),
         coeff p (fun x => boolReal (f x)) S ^ 2) ≤
           m ^ (-1 / 4 : ℝ) * ∑ i, Reindex.influence p f i := by
   …

   Mentions: OAI.Problem313.Reindex.influence, OAI.Problem313.BiasedFourier.weight, OAI.Problem313.BiasedFourier.char, OAI.Problem313.BiasedFourier.coeff, OAI.Problem313.boolReal

3. theorem OAI.Problem313.BiasedFourier.low_degree_estimate line 81

   Source documentation

   The biased Boolean low-degree estimate. No monotonicity or symmetry is required beyond the displayed bound on each coordinate influence.

   theorem low_degree_estimate {p : ℝ} (hp : 0 < p) (hp1 : p < 1)
       (f : (ι → Bool) → Bool) (m : ℝ) (hm : 1 ≤ m)
       (horbit : ∀ i, Reindex.influence p f i ≤ (∑ j, Reindex.influence p f j) / m) :
       (∑ S : Finset ι,
         if S.Nonempty ∧ (S.card : ℝ) ≤ Real.sqrt (p * (1 - p)) * Real.log m / 64
         then coeff p (fun x => boolReal (f x)) S ^ 2 else 0) ≤
           m ^ (-1 / 4 : ℝ) * ∑ i, Reindex.influence p f i := by
   …

   Mentions: OAI.Problem313.Reindex.influence, OAI.Problem313.BiasedFourier.coeff, OAI.Problem313.boolReal

4. theorem OAI.Problem313.BiasedFourier.low_degree_estimate_filter line 92

   Source documentation

   The literal integer-degree filtered-sum form of the low-degree estimate.

   theorem low_degree_estimate_filter {p : ℝ} (hp : 0 < p) (hp1 : p < 1)
       (f : (ι → Bool) → Bool) (m : ℝ) (hm : 1 ≤ m)
       (horbit : ∀ i, Reindex.influence p f i ≤ (∑ j, Reindex.influence p f j) / m) :
       (∑ S ∈ (Finset.univ.filter fun S : Finset ι =>
         1 ≤ S.card ∧ (S.card : ℝ) ≤ Real.sqrt (p * (1 - p)) * Real.log m / 64),
         coeff p (fun x => boolReal (f x)) S ^ 2) ≤
           m ^ (-1 / 4 : ℝ) * ∑ i, Reindex.influence p f i := by
   …

   Mentions: OAI.Problem313.Reindex.influence, OAI.Problem313.BiasedFourier.coeff, OAI.Problem313.boolReal