OAI/Combinatorics/SharpThreshold/LowDegreeCounting.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem313.sum_squares_le_derivative_sum line 14

   Source documentation

   Removing one specified coordinate injects supports containing it into the set of supports of no larger degree. This is the finite-sum step behind the low-degree derivative estimate.

   theorem sum_squares_le_derivative_sum
       {ι : Type u} [Fintype ι] [DecidableEq ι]
       (L : Finset (Finset ι)) (c : Finset ι → ℝ)
       (d : ι → Finset ι → ℝ) (σ k : ℝ) (i : ι)
       (hdegree : ∀ S ∈ L, (S.card : ℝ) ≤ k)
       (hcoeff : ∀ A : Finset ι, i ∉ A → c (insert i A) = σ * d i A) :
       (∑ S ∈ L.filter (fun S => i ∈ S), c S ^ 2) ≤
         σ ^ 2 * ∑ A ∈ (Finset.univ : Finset (Finset ι)).filter
           (fun A => (A.card : ℝ) ≤ k), d i A ^ 2 := by
   …

2. theorem OAI.Problem313.low_degree_derivative_counting line 58

   Source documentation

   Every nonempty support is counted by at least one coordinate. Combining this double counting with the insertion identity bounds its Fourier mass by the sum of the low-degree masses of all coordinate derivatives.

   theorem low_degree_derivative_counting
       {ι : Type u} [Fintype ι] [DecidableEq ι]
       (L : Finset (Finset ι)) (c : Finset ι → ℝ)
       (d : ι → Finset ι → ℝ) (σ k : ℝ)
       (hne : ∀ S ∈ L, S.Nonempty)
       (hdegree : ∀ S ∈ L, (S.card : ℝ) ≤ k)
       (hcoeff : ∀ (i : ι) (A : Finset ι), i ∉ A → c (insert i A) = σ * d i A) :
       (∑ S ∈ L, c S ^ 2) ≤
         σ ^ 2 * ∑ i : ι, ∑ A ∈ (Finset.univ : Finset (Finset ι)).filter
           (fun A => (A.card : ℝ) ≤ k), d i A ^ 2 := by
   …