BlockLowDegree.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem313.average_conditional_low_degree_bound line 21

Source documentation

Averaging the low-degree estimate over exterior configurations preserves its linear influence bound. This is the fixed-block averaging step, before averaging in the choice of the vertex block.

theorem average_conditional_low_degree_bound
    {ι : Type u} [Fintype ι] [DecidableEq ι]
    (P : ι → Prop) [DecidablePred P]
    (p k C : ℝ) (f : (ι → Bool) → Bool)
    (hp : 0 ≤ p) (hp1 : p ≤ 1)
    (hbound : ∀ y : {i // ¬ P i} → Bool,
      (∑ A : Finset {i // P i},
        if A.Nonempty ∧ (A.card : ℝ) ≤ k then
          BiasedFourier.coeff p
            (fun x => boolReal (f (RestrictionInfluence.join P x y))) A ^ 2
        else 0) ≤
      C * ∑ i : {i // P i}, RestrictionInfluence.influence p
…

Mentions: OAI.Problem313.BiasedFourier.coeff, OAI.Problem313.boolReal, OAI.Problem313.RestrictionInfluence.join, OAI.Problem313.RestrictionInfluence.influence

theorem OAI.Problem313.original_mass_bound_of_conditional line 66

Source documentation

The same averaging step with the original Fourier mass supplied by the exact restriction identity. Both premises are equalities/inequalities about the actual canonical product cube, not an abstract replacement for graph probability.

theorem original_mass_bound_of_conditional
    {ι : Type u} [Fintype ι] [DecidableEq ι]
    (P : ι → Prop) [DecidablePred P]
    (p k C M : ℝ) (f : (ι → Bool) → Bool)
    (hp : 0 ≤ p) (hp1 : p ≤ 1)
    (hmass : M =
      ∑ y : {i // ¬ P i} → Bool, BiasedFourier.weight p y *
        ∑ A : Finset {i // P i},
          if A.Nonempty ∧ (A.card : ℝ) ≤ k then
            BiasedFourier.coeff p
              (fun x => boolReal (f (RestrictionInfluence.join P x y))) A ^ 2
          else 0)
…

Mentions: OAI.Problem313.BiasedFourier.weight, OAI.Problem313.BiasedFourier.coeff, OAI.Problem313.boolReal, OAI.Problem313.RestrictionInfluence.join

theorem OAI.Problem313.block_conditional_low_degree_bound_of_estimate line 92

Source documentation

The conditional influence premise for the low-degree theorem follows from vertex invariance and the low-degree estimate on the restricted cube.

theorem block_conditional_low_degree_bound_of_estimate
    {n : ℕ} (B : Finset (Fin n)) [DecidablePred (EdgeTouches B)]
    (hB : 3 ≤ B.card) (f : GraphConfig n → Bool) (hf : VertexInvariant f)
    (p k C : ℝ) (hp : 0 ≤ p) (hp1 : p ≤ 1)
    (hestimate : ∀ g : ({e : GraphEdge n // EdgeTouches B e} → Bool) → Bool,
      (∀ e, Reindex.influence p g e ≤
        (∑ d, Reindex.influence p g d) / (B.card : ℝ)) →
      (∑ A : Finset {e : GraphEdge n // EdgeTouches B e},
        if A.Nonempty ∧ (A.card : ℝ) ≤ k then
          BiasedFourier.coeff p (fun x => boolReal (g x)) A ^ 2 else 0) ≤
      C * ∑ e, Reindex.influence p g e) :
    (∑ y : {e : GraphEdge n // ¬ EdgeTouches B e} → Bool,
…

Mentions: OAI.Problem313.EdgeTouches, OAI.Problem313.GraphConfig, OAI.Problem313.VertexInvariant, OAI.Problem313.GraphEdge, OAI.Problem313.Reindex.influence, OAI.Problem313.BiasedFourier.coeff, OAI.Problem313.boolReal

theorem OAI.Problem313.block_low_degree_bound_of_estimate line 132

Source documentation

Fixed-block Fourier estimate: all exterior Fourier degrees are retained. The only analytic input is the ordinary low-degree estimate on the free cube.

theorem block_low_degree_bound_of_estimate
    {n : ℕ} (B : Finset (Fin n)) [DecidablePred (EdgeTouches B)]
    (hB : 3 ≤ B.card) (f : GraphConfig n → Bool) (hf : VertexInvariant f)
    (p k C : ℝ) (hp : 0 < p) (hp1 : p < 1)
    (hestimate : ∀ g : ({e : GraphEdge n // EdgeTouches B e} → Bool) → Bool,
      (∀ e, Reindex.influence p g e ≤
        (∑ d, Reindex.influence p g d) / (B.card : ℝ)) →
      (∑ A : Finset {e : GraphEdge n // EdgeTouches B e},
        if A.Nonempty ∧ (A.card : ℝ) ≤ k then
          BiasedFourier.coeff p (fun x => boolReal (g x)) A ^ 2 else 0) ≤
      C * ∑ e, Reindex.influence p g e) :
    (∑ S : Finset (GraphEdge n),
…

theorem OAI.Problem313.block_low_degree_bound line 154

Source documentation

The fixed-block low-degree Fourier bound for invariant graph properties. All symmetry, restriction and analytic premises are discharged.

theorem block_low_degree_bound
    {n : ℕ} (B : Finset (Fin n)) [DecidablePred (EdgeTouches B)]
    (hB : 3 ≤ B.card) (f : GraphConfig n → Bool) (hf : VertexInvariant f)
    {p : ℝ} (hp : 0 < p) (hp1 : p < 1) :
    (∑ S : Finset (GraphEdge n),
      if (S.filter (EdgeTouches B)).Nonempty ∧
          ((S.filter (EdgeTouches B)).card : ℝ) ≤
            Real.sqrt (p * (1 - p)) * Real.log (B.card : ℝ) / 64 then
        BiasedFourier.coeff p (fun x => boolReal (f x)) S ^ 2 else 0) ≤
      (B.card : ℝ) ^ (-1 / 4 : ℝ) *
        ∑ e : {e : GraphEdge n // EdgeTouches B e}, edgeInfluence p f e.val := by
…

Mentions: OAI.Problem313.EdgeTouches, OAI.Problem313.GraphConfig, OAI.Problem313.VertexInvariant, OAI.Problem313.GraphEdge, OAI.Problem313.BiasedFourier.coeff, OAI.Problem313.boolReal, OAI.Problem313.edgeInfluence

theorem OAI.Problem313.block_low_degree_bound_filter line 172

Source documentation

Filtered finite-sum version of the fixed-block low-degree bound.

theorem block_low_degree_bound_filter
    {n : ℕ} (B : Finset (Fin n)) [DecidablePred (EdgeTouches B)]
    (hB : 3 ≤ B.card) (f : GraphConfig n → Bool) (hf : VertexInvariant f)
    {p : ℝ} (hp : 0 < p) (hp1 : p < 1) :
    (∑ S ∈ Finset.univ.filter (fun S : Finset (GraphEdge n) =>
      1 ≤ (S.filter (EdgeTouches B)).card ∧
        ((S.filter (EdgeTouches B)).card : ℝ) ≤
          Real.sqrt (p * (1 - p)) * Real.log (B.card : ℝ) / 64),
      BiasedFourier.coeff p (fun x => boolReal (f x)) S ^ 2) ≤
      (B.card : ℝ) ^ (-1 / 4 : ℝ) *
        ∑ e ∈ Finset.univ.filter (EdgeTouches B), edgeInfluence p f e := by
…