OAI/Combinatorics/SharpThreshold/FourierSupportSplit.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem313.BiasedFourier.sum_support_disjSum line 15

   Source documentation

   Reindex all Fourier supports on a sum coordinate set by their two parts.

   theorem sum_support_disjSum (a : Finset (ι ⊕ κ) → M) :
       (∑ S : Finset (ι ⊕ κ), a S) =
         ∑ A : Finset ι, ∑ D : Finset κ, a (A.disjSum D) := by
   …

2. theorem OAI.Problem313.BiasedFourier.sum_support_condition_disjSum line 23

   Source documentation

   Restricting the free-coordinate support commutes with the support split.

   theorem sum_support_condition_disjSum (a : Finset (ι ⊕ κ) → M)
       (P : Finset ι → Prop) [DecidablePred P] :
       (∑ S : Finset (ι ⊕ κ), if P S.toLeft then a S else 0) =
         ∑ A : Finset ι, if P A then
           ∑ D : Finset κ, a (A.disjSum D) else 0 := by
   …

3. theorem OAI.Problem313.BiasedFourier.sum_support_filter_disjSum line 33

   Source documentation

   Filter formulation of the same identity, useful for degree cutoffs.

   theorem sum_support_filter_disjSum (a : Finset (ι ⊕ κ) → M)
       (P : Finset ι → Prop) [DecidablePred P] :
       (∑ S ∈ Finset.univ.filter (fun S : Finset (ι ⊕ κ) => P S.toLeft), a S) =
         ∑ A ∈ Finset.univ.filter P, ∑ D : Finset κ, a (A.disjSum D) := by
   …