BooleanProjection.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem313.BiasedFourier.booleanDifference_project_energy_le line 19

Source documentation

Low-degree projection bound for a Boolean coordinate difference, with the pivotal probability expressed by the shared generic influence definition.

theorem booleanDifference_project_energy_le {p : ℝ} (hp : 0 < p) (hp1 : p < 1)
    (rho k : ℝ) (hrho : 0 < rho) (hrho1 : rho ≤ 1)
    (hnoise : ∀ a : Finset ι → ℝ,
      (∑ x, weight p x *
        (∑ S, rho ^ S.card * a S * char p S x) ^ 4) ≤
          (∑ S, (a S) ^ 2) ^ 2)
    (L : Finset (Finset ι)) (f : (ι → Bool) → Bool) (i : ι)
    (hdegree : ∀ S ∈ L, (S.card : ℝ) ≤ k) :
    (∑ S ∈ L, (coeff p
      (fun x => boolReal (f (Function.update x i true)) -
        boolReal (f (Function.update x i false))) S) ^ 2) ≤
      rho ^ (-2 * k) * (Reindex.influence p f i) ^ (3 / 2 : ℝ) := by
…

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

theorem OAI.Problem313.BiasedFourier.booleanDifference_lowDegree_energy_le line 49

Source documentation

The Boolean coordinate-difference energy bound with a real degree cutoff.

theorem booleanDifference_lowDegree_energy_le {p : ℝ} (hp : 0 < p) (hp1 : p < 1)
    (rho k : ℝ) (hrho : 0 < rho) (hrho1 : rho ≤ 1)
    (hnoise : ∀ a : Finset ι → ℝ,
      (∑ x, weight p x *
        (∑ S, rho ^ S.card * a S * char p S x) ^ 4) ≤
          (∑ S, (a S) ^ 2) ^ 2)
    (f : (ι → Bool) → Bool) (i : ι) :
    (∑ S ∈ (Finset.univ.filter fun S : Finset ι => (S.card : ℝ) ≤ k),
      (coeff p (fun x => boolReal (f (Function.update x i true)) -
        boolReal (f (Function.update x i false))) S) ^ 2) ≤
      rho ^ (-2 * k) * (Reindex.influence p f i) ^ (3 / 2 : ℝ) := by
…

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