OAI/Combinatorics/SharpThreshold/LowDegreeBounds.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem313.lowDegree_mass_le_incident_mass line 16

   Source documentation

   Every nonempty low-degree Fourier support is counted by at least one of its incident coordinate sums. This is purely finite, nonnegative double counting.

   theorem lowDegree_mass_le_incident_mass
       {ι : Type u} [Fintype ι] [DecidableEq ι]
       (a : Finset ι → ℝ) (ha : ∀ S, 0 ≤ a S) (k : ℝ) :
       (∑ S : Finset ι, if S.Nonempty ∧ (S.card : ℝ) ≤ k then a S else 0) ≤
         ∑ i : ι, ∑ S : Finset ι, if i ∈ S ∧ (S.card : ℝ) ≤ k then a S else 0 := by
   …

2. theorem OAI.Problem313.lowDegree_mass_le_of_coordinate_bound line 46

   Source documentation

   Assemble coordinatewise low-degree estimates without any choice of a single coordinate common to all supports.

   theorem lowDegree_mass_le_of_coordinate_bound
       {ι : Type u} [Fintype ι] [DecidableEq ι]
       (a : Finset ι → ℝ) (ha : ∀ S, 0 ≤ a S) (k C : ℝ)
       (J : ι → ℝ)
       (hcoord : ∀ i, (∑ S : Finset ι,
         if i ∈ S ∧ (S.card : ℝ) ≤ k then a S else 0) ≤ C * J i) :
       (∑ S : Finset ι, if S.Nonempty ∧ (S.card : ℝ) ≤ k then a S else 0) ≤
         C * ∑ i : ι, J i := by
   …

3. theorem OAI.Problem313.lowDegree_mass_eq_zero_of_lt_one line 62

   Source documentation

   A cutoff below one contains no nonconstant Boolean Fourier supports.

   theorem lowDegree_mass_eq_zero_of_lt_one
       {ι : Type u} [Fintype ι] [DecidableEq ι]
       (a : Finset ι → ℝ) {k : ℝ} (hk : k < 1) :
       (∑ S : Finset ι, if S.Nonempty ∧ (S.card : ℝ) ≤ k then a S else 0) = 0 := by
   …

4. theorem OAI.Problem313.incident_mass_le_erase_mass line 76

   Source documentation

   Erasing a fixed coordinate injects supports containing it into supports of no larger degree. This transports a derivative coefficient identity to a low-degree mass bound, without changing the ambient coordinate type.

   theorem incident_mass_le_erase_mass
       {ι : Type u} [Fintype ι] [DecidableEq ι]
       (a b : Finset ι → ℝ) (hb : ∀ T, 0 ≤ b T) (i : ι) (k C : ℝ)
       (hC : 0 ≤ C)
       (hderiv : ∀ S, i ∈ S → a S = C * b (S.erase i)) :
       (∑ S : Finset ι, if i ∈ S ∧ (S.card : ℝ) ≤ k then a S else 0) ≤
         C * ∑ T : Finset ι, if (T.card : ℝ) ≤ k then b T else 0 := by
   …

5. theorem OAI.Problem313.lowDegree_bound_of_projection line 117

   Source documentation

   The complete low-degree estimate once the analytic Fourier ingredients are supplied: the derivative coefficient identity and the low-degree projection bound. All incidence counting, bias constants, and the small/large total-influence split are discharged here.

   theorem lowDegree_bound_of_projection
       {ι : Type u} [Fintype ι] [DecidableEq ι]
       (a : Finset ι → ℝ) (b : ι → Finset ι → ℝ) (J : ι → ℝ)
       (σ m : ℝ) (hσ : 0 < σ) (hσhalf : σ ≤ 1 / 2) (hm : 1 ≤ m)
       (ha : ∀ S, 0 ≤ a S) (hb : ∀ i S, 0 ≤ b i S)
       (hJ : ∀ i, 0 ≤ J i) (horbit : ∀ i, J i ≤ (∑ j, J j) / m)
       (henergy : (∑ S : Finset ι, a S) ≤ 1)
       (hderiv : ∀ i S, i ∈ S → a S = σ ^ 2 * b i (S.erase i))
       (hprojection : ∀ i,
         (∑ S : Finset ι, if (S.card : ℝ) ≤ σ * Real.log m / 64 then b i S else 0) ≤
           (σ / 4) ^ (-(2 : ℝ) * (σ * Real.log m / 64)) * (J i) ^ (3 / 2 : ℝ)) :
       (∑ S : Finset ι,
   …