3.3. Restrictions🔗

Lemma3.3.1

Statement uses 5

Statement dependency previews

Preview

Definition 1.2.2

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

Used by 4

Reverse dependency previews

Preview

Lemma 3.3.2

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

Tagssection-3-3supportfidelity-conservative-generalization

Finite-index sign-cube Fourier formulas. Let I be a finite set. For x\in\{-1,1\}^{I} and A\subseteq I, write x^A=\prod_{i\in A}x_i. For every g:\{-1,1\}^{I}\to\mathbb R, define \widehat g(A) =\mathbb E_{\boldsymbol{x}\sim\{-1,1\}^{I}} [g(\boldsymbol{x})\boldsymbol{x}^{A}]. Then g(x)=\sum_{A\subseteq I}\widehat g(A)x^A, \qquad \mathbb E[g]=\widehat g(\varnothing), \qquad \mathbb E[g^2]=\sum_{A\subseteq I}\widehat g(A)^2. For I=[n], these are the monomials, Fourier coefficients, Fourier expansion, constant-coefficient formula, and Parseval formula of Chapter 1.

Lean code for Lemma3.3.1●9 declarations

abbrevdefined in FABL/Chapter03/Restrictions.lean

complete

abbrev FABL.IndexedSignCube.{u_1} (ι : Type u_1) : Type u_1

abbrev FABL.IndexedSignCube.{u_1}
  (ι : Type u_1) : Type u_1

A sign cube whose coordinates are indexed by an arbitrary type.

defdefined in FABL/Chapter03/Restrictions.lean

complete

def FABL.indexedMonomial.{u_1} {ι : Type u_1} (S : Finset ι)
  (x : FABL.IndexedSignCube ι) : ℝ

def FABL.indexedMonomial.{u_1} {ι : Type u_1}
  (S : Finset ι)
  (x : FABL.IndexedSignCube ι) : ℝ

The monomial indexed by `S` on an arbitrary finitely indexed sign cube.

defdefined in FABL/Chapter03/Restrictions.lean

complete

def FABL.indexedSignMonomialChar.{u_1} {ι : Type u_1} (S : Finset ι) :
  AddChar (Additive (FABL.IndexedSignCube ι)) ℝ

def FABL.indexedSignMonomialChar.{u_1}
  {ι : Type u_1} (S : Finset ι) :
  AddChar
    (Additive (FABL.IndexedSignCube ι)) ℝ

An indexed sign-cube monomial bundled as an additive character.

defdefined in FABL/Chapter03/Restrictions.lean

complete

def FABL.indexedWalshBasis.{u_1} (ι : Type u_1) [Fintype ι]
  [DecidableEq ι] :
  Module.Basis (Finset ι) ℝ (FABL.IndexedSignCube ι → ℝ)

def FABL.indexedWalshBasis.{u_1}
  (ι : Type u_1) [Fintype ι]
  [DecidableEq ι] :
  Module.Basis (Finset ι) ℝ
    (FABL.IndexedSignCube ι → ℝ)

Mathlib's finite-character basis, indexed by finite coordinate sets.

defdefined in FABL/Chapter03/Restrictions.lean

complete

def FABL.indexedFourierCoeff.{u_1} {ι : Type u_1} [Fintype ι]
  [DecidableEq ι] (f : FABL.IndexedSignCube ι → ℝ) (S : Finset ι) : ℝ

def FABL.indexedFourierCoeff.{u_1}
  {ι : Type u_1} [Fintype ι]
  [DecidableEq ι]
  (f : FABL.IndexedSignCube ι → ℝ)
  (S : Finset ι) : ℝ

The uniform Fourier coefficient on an arbitrary finitely indexed sign cube.

theoremdefined in FABL/Chapter03/Restrictions.lean

complete

theorem FABL.indexed_fourier_expansion.{u_1} {ι : Type u_1} [Fintype ι]
  [DecidableEq ι] (f : FABL.IndexedSignCube ι → ℝ)
  (x : FABL.IndexedSignCube ι) :
  f x = ∑ S, FABL.indexedFourierCoeff f S * FABL.indexedMonomial S x

theorem FABL.indexed_fourier_expansion.{u_1}
  {ι : Type u_1} [Fintype ι]
  [DecidableEq ι]
  (f : FABL.IndexedSignCube ι → ℝ)
  (x : FABL.IndexedSignCube ι) :
  f x =
    ∑ S,
      FABL.indexedFourierCoeff f S *
        FABL.indexedMonomial S x

Fourier expansion on an arbitrary finitely indexed sign cube.

theoremdefined in FABL/Chapter03/Restrictions.lean

complete

theorem FABL.expect_eq_indexedFourierCoeff_empty.{u_1} {ι : Type u_1}
  [Fintype ι] [DecidableEq ι] (f : FABL.IndexedSignCube ι → ℝ) :
  (Finset.univ.expect fun x => f x) = FABL.indexedFourierCoeff f ∅

theorem FABL.expect_eq_indexedFourierCoeff_empty.{u_1}
  {ι : Type u_1} [Fintype ι]
  [DecidableEq ι]
  (f : FABL.IndexedSignCube ι → ℝ) :
  (Finset.univ.expect fun x => f x) =
    FABL.indexedFourierCoeff f ∅

The mean is the empty-set Fourier coefficient on every finitely indexed sign cube.

theoremdefined in FABL/Chapter03/Restrictions.lean

complete

theorem FABL.indexed_plancherel.{u_1} {ι : Type u_1} [Fintype ι] [DecidableEq ι]
  (f g : FABL.IndexedSignCube ι → ℝ) :
  (Finset.univ.expect fun x => f x * g x) =
    ∑ S, FABL.indexedFourierCoeff f S * FABL.indexedFourierCoeff g S

theorem FABL.indexed_plancherel.{u_1}
  {ι : Type u_1} [Fintype ι]
  [DecidableEq ι]
  (f g : FABL.IndexedSignCube ι → ℝ) :
  (Finset.univ.expect fun x =>
      f x * g x) =
    ∑ S,
      FABL.indexedFourierCoeff f S *
        FABL.indexedFourierCoeff g S

Plancherel's identity on an arbitrary finitely indexed sign cube.

theoremdefined in FABL/Chapter03/Restrictions.lean

complete

theorem FABL.indexed_parseval.{u_1} {ι : Type u_1} [Fintype ι] [DecidableEq ι]
  (f : FABL.IndexedSignCube ι → ℝ) :
  (Finset.univ.expect fun x => f x ^ 2) =
    ∑ S, FABL.indexedFourierCoeff f S ^ 2

theorem FABL.indexed_parseval.{u_1} {ι : Type u_1}
  [Fintype ι] [DecidableEq ι]
  (f : FABL.IndexedSignCube ι → ℝ) :
  (Finset.univ.expect fun x => f x ^ 2) =
    ∑ S, FABL.indexedFourierCoeff f S ^ 2

Parseval's identity on an arbitrary finitely indexed sign cube.

Lemma3.3.2

uses 1

Used by 2

Reverse dependency previews

Preview

Definition 3.3.3

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

Tagssection-3-3supportfidelity-exact

Coordinate and frequency splitting. Let J\subseteq[n] and \bar J=[n]\setminus J. Every x\in\{-1,1\}^n has a unique decomposition x=(y,z), \qquad y\in\{-1,1\}^{J}, \quad z\in\{-1,1\}^{\bar J}. Every U\subseteq[n] has a unique decomposition U=S\mathbin{\dot\cup}T, \qquad S=U\cap J\subseteq J, \quad T=U\cap\bar J\subseteq\bar J. Under these decompositions, x^U=y^S z^T.

Lean code for Lemma3.3.2●15 declarations

abbrevdefined in FABL/Chapter03/Restrictions.lean

complete

abbrev FABL.FixedIndex {n : ℕ} (J : Finset (Fin n)) : Type

abbrev FABL.FixedIndex {n : ℕ}
  (J : Finset (Fin n)) : Type

The coordinates outside `J`, representing the book's `J̄`.

abbrevdefined in FABL/Chapter03/Restrictions.lean

complete

abbrev FABL.FreeSignCube {n : ℕ} (J : Finset (Fin n)) : Type

abbrev FABL.FreeSignCube {n : ℕ}
  (J : Finset (Fin n)) : Type

Assignments to the free coordinates in `J`.

abbrevdefined in FABL/Chapter03/Restrictions.lean

complete

abbrev FABL.FixedSignCube {n : ℕ} (J : Finset (Fin n)) : Type

abbrev FABL.FixedSignCube {n : ℕ}
  (J : Finset (Fin n)) : Type

Assignments to the fixed coordinates outside `J`.

defdefined in FABL/Chapter03/Restrictions.lean

complete

def FABL.signCubeSplitEquiv {n : ℕ} (J : Finset (Fin n)) :
  FABL.SignCube n ≃ FABL.FreeSignCube J × FABL.FixedSignCube J

def FABL.signCubeSplitEquiv {n : ℕ}
  (J : Finset (Fin n)) :
  FABL.SignCube n ≃
    FABL.FreeSignCube J ×
      FABL.FixedSignCube J

Mathlib's canonical splitting of a full sign cube into the coordinates in `J` and outside
`J`.

defdefined in FABL/Chapter03/Restrictions.lean

complete

def FABL.combineSignCube {n : ℕ} (J : Finset (Fin n))
  (y : FABL.FreeSignCube J) (z : FABL.FixedSignCube J) : FABL.SignCube n

def FABL.combineSignCube {n : ℕ}
  (J : Finset (Fin n))
  (y : FABL.FreeSignCube J)
  (z : FABL.FixedSignCube J) :
  FABL.SignCube n

Combine assignments on `J` and its complement into a full sign string.

defdefined in FABL/Chapter03/Restrictions.lean

complete

def FABL.liftFreeFrequency {n : ℕ} {J : Finset (Fin n)} (S : Finset ↥J) :
  Finset (Fin n)

def FABL.liftFreeFrequency {n : ℕ}
  {J : Finset (Fin n)} (S : Finset ↥J) :
  Finset (Fin n)

Embed a frequency on the free coordinates into the full coordinate set.

defdefined in FABL/Chapter03/Restrictions.lean

complete

def FABL.liftFixedFrequency {n : ℕ} {J : Finset (Fin n)}
  (T : Finset (FABL.FixedIndex J)) : Finset (Fin n)

def FABL.liftFixedFrequency {n : ℕ}
  {J : Finset (Fin n)}
  (T : Finset (FABL.FixedIndex J)) :
  Finset (Fin n)

Embed a frequency on the fixed coordinates into the full coordinate set.

defdefined in FABL/Chapter03/Restrictions.lean

complete

def FABL.freeFrequencyPart {n : ℕ} (J U : Finset (Fin n)) : Finset ↥J

def FABL.freeFrequencyPart {n : ℕ}
  (J U : Finset (Fin n)) : Finset ↥J

The part of an ambient frequency supported on the free coordinates `J`.

defdefined in FABL/Chapter03/Restrictions.lean

complete

def FABL.fixedFrequencyPart {n : ℕ} (J U : Finset (Fin n)) :
  Finset (FABL.FixedIndex J)

def FABL.fixedFrequencyPart {n : ℕ}
  (J U : Finset (Fin n)) :
  Finset (FABL.FixedIndex J)

The part of an ambient frequency supported outside the free coordinates `J`.

theoremdefined in FABL/Chapter03/Restrictions.lean

complete

theorem FABL.disjoint_liftFreeFrequency_liftFixedFrequency {n : ℕ}
  {J : Finset (Fin n)} (S : Finset ↥J)
  (T : Finset (FABL.FixedIndex J)) :
  Disjoint (FABL.liftFreeFrequency S) (FABL.liftFixedFrequency T)

theorem FABL.disjoint_liftFreeFrequency_liftFixedFrequency
  {n : ℕ} {J : Finset (Fin n)}
  (S : Finset ↥J)
  (T : Finset (FABL.FixedIndex J)) :
  Disjoint (FABL.liftFreeFrequency S)
    (FABL.liftFixedFrequency T)

Frequencies lifted from `J` and its complement are disjoint.

theoremdefined in FABL/Chapter03/Restrictions.lean

complete

theorem FABL.disjoint_liftFreeFrequencyPart_liftFixedFrequencyPart {n : ℕ}
  (J U : Finset (Fin n)) :
  Disjoint (FABL.liftFreeFrequency (FABL.freeFrequencyPart J U))
    (FABL.liftFixedFrequency (FABL.fixedFrequencyPart J U))

theorem FABL.disjoint_liftFreeFrequencyPart_liftFixedFrequencyPart
  {n : ℕ} (J U : Finset (Fin n)) :
  Disjoint
    (FABL.liftFreeFrequency
      (FABL.freeFrequencyPart J U))
    (FABL.liftFixedFrequency
      (FABL.fixedFrequencyPart J U))

The lifted free and fixed parts of an ambient frequency are disjoint.

theoremdefined in FABL/Chapter03/Restrictions.lean

complete

theorem FABL.liftFreeFrequencyPart_union_liftFixedFrequencyPart {n : ℕ}
  (J U : Finset (Fin n)) :
  FABL.liftFreeFrequency (FABL.freeFrequencyPart J U) ∪
      FABL.liftFixedFrequency (FABL.fixedFrequencyPart J U) =
    U

theorem FABL.liftFreeFrequencyPart_union_liftFixedFrequencyPart
  {n : ℕ} (J U : Finset (Fin n)) :
  FABL.liftFreeFrequency
        (FABL.freeFrequencyPart J U) ∪
      FABL.liftFixedFrequency
        (FABL.fixedFrequencyPart J U) =
    U

Splitting an ambient frequency along `J` and lifting both parts recovers it.

theoremdefined in FABL/Chapter03/Restrictions.lean

complete

theorem FABL.existsUnique_frequency_split {n : ℕ} (J U : Finset (Fin n)) :
  ∃! ST, FABL.liftFreeFrequency ST.1 ∪ FABL.liftFixedFrequency ST.2 = U

theorem FABL.existsUnique_frequency_split {n : ℕ}
  (J U : Finset (Fin n)) :
  ∃! ST,
    FABL.liftFreeFrequency ST.1 ∪
        FABL.liftFixedFrequency ST.2 =
      U

Every ambient frequency has a unique decomposition into frequencies on `J` and its
complement.

theoremdefined in FABL/Chapter03/Restrictions.lean

complete

theorem FABL.indexedMonomial_lift_union_combine {n : ℕ} {J : Finset (Fin n)}
  (S : Finset ↥J) (T : Finset (FABL.FixedIndex J))
  (y : FABL.FreeSignCube J) (z : FABL.FixedSignCube J) :
  FABL.monomial (FABL.liftFreeFrequency S ∪ FABL.liftFixedFrequency T)
      (FABL.combineSignCube J y z) =
    FABL.indexedMonomial S y * FABL.indexedMonomial T z

theorem FABL.indexedMonomial_lift_union_combine
  {n : ℕ} {J : Finset (Fin n)}
  (S : Finset ↥J)
  (T : Finset (FABL.FixedIndex J))
  (y : FABL.FreeSignCube J)
  (z : FABL.FixedSignCube J) :
  FABL.monomial
      (FABL.liftFreeFrequency S ∪
        FABL.liftFixedFrequency T)
      (FABL.combineSignCube J y z) =
    FABL.indexedMonomial S y *
      FABL.indexedMonomial T z

A monomial on a composite string factors into its free and fixed parts.

theoremdefined in FABL/Chapter03/Restrictions.lean

complete

theorem FABL.monomial_liftFreeFrequency_combine {n : ℕ} {J : Finset (Fin n)}
  (S : Finset ↥J) (y : FABL.FreeSignCube J) (z : FABL.FixedSignCube J) :
  FABL.monomial (FABL.liftFreeFrequency S)
      (FABL.combineSignCube J y z) =
    FABL.indexedMonomial S y

theorem FABL.monomial_liftFreeFrequency_combine
  {n : ℕ} {J : Finset (Fin n)}
  (S : Finset ↥J)
  (y : FABL.FreeSignCube J)
  (z : FABL.FixedSignCube J) :
  FABL.monomial (FABL.liftFreeFrequency S)
      (FABL.combineSignCube J y z) =
    FABL.indexedMonomial S y

A monomial supported on the free coordinates ignores the fixed assignment.

Definition3.3.3

uses 1

Used by 2

Reverse dependency previews

Preview

Lemma 3.3.4

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

Tagssection-3-3fidelity-exact

Definition 3.18. Let f:\{-1,1\}^n\to\mathbb R and let (J,\bar J) be a partition of [n], with \bar J=[n]\setminus J. For z\in\{-1,1\}^{\bar J}, write f_{J\mid z}:\{-1,1\}^{J}\to\mathbb R for the subfunction obtained by fixing the coordinates in \bar J to the bit values z. If y\in\{-1,1\}^{J} and z\in\{-1,1\}^{\bar J}, write (y,z)\in\{-1,1\}^n for their composite string. Thus f_{J\mid z}(y)=f(y,z). When the partition is understood, one may write simply f_{\mid z}.

Lean code for Definition3.3.3●1 definition

defdefined in FABL/Chapter03/Restrictions.lean

complete

def FABL.signRestriction.{u_1} {n : ℕ} {α : Type u_1}
  (f : FABL.SignCube n → α) (J : Finset (Fin n))
  (z : FABL.FixedSignCube J) : FABL.FreeSignCube J → α

def FABL.signRestriction.{u_1} {n : ℕ}
  {α : Type u_1} (f : FABL.SignCube n → α)
  (J : Finset (Fin n))
  (z : FABL.FixedSignCube J) :
  FABL.FreeSignCube J → α

O'Donnell, Definition 3.18, conservatively generalized in the codomain: restrict a function
to the coordinates in `J` by fixing all complementary coordinates to `z`.

Lemma3.3.4

Statement uses 2

Statement dependency previews

Preview

Theorem 1.2.3

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 0✓L∃∀N

Tagssection-3-3fidelity-exact

Example 3.19. Let f:\{-1,1\}^4\to\{-1,1\} be defined by f(x)=1 \quad\Longleftrightarrow\quad x_3=x_4=-1 \ \text{or}\ x_1\ge x_2\ge x_3\ge x_4 \ \text{or}\ x_1\le x_2\le x_3\le x_4. \tag{3.2} Its Fourier expansion is \begin{aligned} f(x)={}&\frac18-\frac18x_1+\frac18x_2-\frac18x_3-\frac18x_4\\ &+\frac38x_1x_2+\frac18x_1x_3-\frac38x_1x_4 +\frac38x_2x_3-\frac18x_2x_4+\frac58x_3x_4\\ &+\frac18x_1x_2x_3+\frac18x_1x_2x_4-\frac18x_1x_3x_4 +\frac18x_2x_3x_4-\frac18x_1x_2x_3x_4. \end{aligned} \tag{3.3} Fix x_3=1 and x_4=-1, and let f'=f_{\{1,2\}\mid(1,-1)}. Then f'(x_1,x_2)=1\Longleftrightarrow x_1=x_2=1, so f'=\min_2, with Fourier expansion f'(x_1,x_2)=\min_2(x_1,x_2) =-\frac12+\frac12x_1+\frac12x_2+\frac12x_1x_2. \tag{3.4} In particular, the terms contributing to the coefficient on x_1 after this restriction are -\frac18x_1, \quad +\frac18x_1x_3, \quad -\frac38x_1x_4, \quad -\frac18x_1x_3x_4, and their restricted coefficients sum to -\frac18+\frac18+\frac38+\frac18=\frac12.

Lean code for Lemma3.3.4●14 declarations

defdefined in FABL/Chapter03/Restrictions.lean

complete

def FABL.example3_19Predicate (x : FABL.SignCube 4) : Prop

def FABL.example3_19Predicate
  (x : FABL.SignCube 4) : Prop

The predicate in equation (3.2), with Lean's zero-based coordinates corresponding to the
book's `x₁, …, x₄`.

defdefined in FABL/Chapter03/Restrictions.lean

complete

def FABL.example3_19Function : FABL.BooleanFunction 4

def FABL.example3_19Function :
  FABL.BooleanFunction 4

O'Donnell, Example 3.19, equation (3.2).

theoremdefined in FABL/Chapter03/Restrictions.lean

complete

theorem FABL.example3_19Function_eq_one_iff (x : FABL.SignCube 4) :
  FABL.example3_19Function x = 1 ↔ FABL.example3_19Predicate x

theorem FABL.example3_19Function_eq_one_iff
  (x : FABL.SignCube 4) :
  FABL.example3_19Function x = 1 ↔
    FABL.example3_19Predicate x

Equation (3.2) stated as the defining `+1` criterion.

theoremdefined in FABL/Chapter03/Restrictions.lean

complete

theorem FABL.example3_19_fourier_expansion (x : FABL.SignCube 4) :
  FABL.signValue (FABL.example3_19Function x) =
    1 / 8 - 1 / 8 * FABL.signValue (x 0) +
                                1 / 8 * FABL.signValue (x 1) -
                              1 / 8 * FABL.signValue (x 2) -
                            1 / 8 * FABL.signValue (x 3) +
                          3 / 8 * FABL.signValue (x 0) *
                            FABL.signValue (x 1) +
                        1 / 8 * FABL.signValue (x 0) *
                          FABL.signValue (x 2) -
                      3 / 8 * FABL.signValue (x 0) *
                        FABL.signValue (x 3) +
                    3 / 8 * FABL.signValue (x 1) *
                      FABL.signValue (x 2) -
                  1 / 8 * FABL.signValue (x 1) * FABL.signValue (x 3) +
                5 / 8 * FABL.signValue (x 2) * FABL.signValue (x 3) +
              1 / 8 * FABL.signValue (x 0) * FABL.signValue (x 1) *
                FABL.signValue (x 2) +
            1 / 8 * FABL.signValue (x 0) * FABL.signValue (x 1) *
              FABL.signValue (x 3) -
          1 / 8 * FABL.signValue (x 0) * FABL.signValue (x 2) *
            FABL.signValue (x 3) +
        1 / 8 * FABL.signValue (x 1) * FABL.signValue (x 2) *
          FABL.signValue (x 3) -
      1 / 8 * FABL.signValue (x 0) * FABL.signValue (x 1) *
          FABL.signValue (x 2) *
        FABL.signValue (x 3)

theorem FABL.example3_19_fourier_expansion
  (x : FABL.SignCube 4) :
  FABL.signValue
      (FABL.example3_19Function x) =
    1 / 8 - 1 / 8 * FABL.signValue (x 0) +
                                1 / 8 *
                                  FABL.signValue
                                    (x
                                      1) -
                              1 / 8 *
                                FABL.signValue
                                  (x 2) -
                            1 / 8 *
                              FABL.signValue
                                (x 3) +
                          3 / 8 *
                              FABL.signValue
                                (x 0) *
                            FABL.signValue
                              (x 1) +
                        1 / 8 *
                            FABL.signValue
                              (x 0) *
                          FABL.signValue
                            (x 2) -
                      3 / 8 *
                          FABL.signValue
                            (x 0) *
                        FABL.signValue
                          (x 3) +
                    3 / 8 *
                        FABL.signValue
                          (x 1) *
                      FABL.signValue
                        (x 2) -
                  1 / 8 *
                      FABL.signValue
                        (x 1) *
                    FABL.signValue (x 3) +
                5 / 8 *
                    FABL.signValue (x 2) *
                  FABL.signValue (x 3) +
              1 / 8 *
                    FABL.signValue (x 0) *
                  FABL.signValue (x 1) *
                FABL.signValue (x 2) +
            1 / 8 * FABL.signValue (x 0) *
                FABL.signValue (x 1) *
              FABL.signValue (x 3) -
          1 / 8 * FABL.signValue (x 0) *
              FABL.signValue (x 2) *
            FABL.signValue (x 3) +
        1 / 8 * FABL.signValue (x 1) *
            FABL.signValue (x 2) *
          FABL.signValue (x 3) -
      1 / 8 * FABL.signValue (x 0) *
            FABL.signValue (x 1) *
          FABL.signValue (x 2) *
        FABL.signValue (x 3)

O'Donnell, Example 3.19, equation (3.3): the complete Fourier expansion of the four-bit
function.

defdefined in FABL/Chapter03/Restrictions.lean

complete

def FABL.example3_19FreeCoordinates : Finset (Fin 4)

def FABL.example3_19FreeCoordinates :
  Finset (Fin 4)

The free coordinates `{1,2}` from Example 3.19, represented with Lean's zero-based
indices.

defdefined in FABL/Chapter03/Restrictions.lean

complete

def FABL.example3_19First : ↥FABL.example3_19FreeCoordinates

def FABL.example3_19First :
  ↥FABL.example3_19FreeCoordinates

The first free coordinate in Example 3.19.

defdefined in FABL/Chapter03/Restrictions.lean

complete

def FABL.example3_19Second : ↥FABL.example3_19FreeCoordinates

def FABL.example3_19Second :
  ↥FABL.example3_19FreeCoordinates

The second free coordinate in Example 3.19.

defdefined in FABL/Chapter03/Restrictions.lean

complete

def FABL.example3_19FixedAssignment :
  FABL.FixedSignCube FABL.example3_19FreeCoordinates

def FABL.example3_19FixedAssignment :
  FABL.FixedSignCube
    FABL.example3_19FreeCoordinates

The complementary assignment `x₃ = 1, x₄ = -1` from Example 3.19.

defdefined in FABL/Chapter03/Restrictions.lean

complete

def FABL.example3_19TwoBitInput
  (y : FABL.FreeSignCube FABL.example3_19FreeCoordinates) :
  FABL.SignCube 2

def FABL.example3_19TwoBitInput
  (y :
    FABL.FreeSignCube
      FABL.example3_19FreeCoordinates) :
  FABL.SignCube 2

Reindex the two free coordinates of Example 3.19 by `Fin 2`.

theoremdefined in FABL/Chapter03/Restrictions.lean

complete

theorem FABL.example3_19_restriction_eq_orFunction :
  FABL.signRestriction FABL.example3_19Function
      FABL.example3_19FreeCoordinates FABL.example3_19FixedAssignment =
    fun y => FABL.orFunction 2 (FABL.example3_19TwoBitInput y)

theorem FABL.example3_19_restriction_eq_orFunction :
  FABL.signRestriction
      FABL.example3_19Function
      FABL.example3_19FreeCoordinates
      FABL.example3_19FixedAssignment =
    fun y =>
    FABL.orFunction 2
      (FABL.example3_19TwoBitInput y)

The restriction in Example 3.19 is the two-bit minimum function, represented by the already
established Boolean `orFunction` in the book's `-1 = True` convention.

theoremdefined in FABL/Chapter03/Restrictions.lean

complete

theorem FABL.example3_19_restriction_eq_one_iff
  (y : FABL.FreeSignCube FABL.example3_19FreeCoordinates) :
  FABL.signRestriction FABL.example3_19Function
        FABL.example3_19FreeCoordinates FABL.example3_19FixedAssignment
        y =
      1 ↔
    y FABL.example3_19First = 1 ∧ y FABL.example3_19Second = 1

theorem FABL.example3_19_restriction_eq_one_iff
  (y :
    FABL.FreeSignCube
      FABL.example3_19FreeCoordinates) :
  FABL.signRestriction
        FABL.example3_19Function
        FABL.example3_19FreeCoordinates
        FABL.example3_19FixedAssignment
        y =
      1 ↔
    y FABL.example3_19First = 1 ∧
      y FABL.example3_19Second = 1

The defining `+1` criterion for the restricted two-bit function in Example 3.19.

theoremdefined in FABL/Chapter03/Restrictions.lean

complete

theorem FABL.example3_19_restriction_fourier_expansion
  (y : FABL.FreeSignCube FABL.example3_19FreeCoordinates) :
  FABL.signValue
      (FABL.signRestriction FABL.example3_19Function
        FABL.example3_19FreeCoordinates FABL.example3_19FixedAssignment
        y) =
    -1 / 2 + 1 / 2 * FABL.signValue (y FABL.example3_19First) +
        1 / 2 * FABL.signValue (y FABL.example3_19Second) +
      1 / 2 * FABL.signValue (y FABL.example3_19First) *
        FABL.signValue (y FABL.example3_19Second)

theorem FABL.example3_19_restriction_fourier_expansion
  (y :
    FABL.FreeSignCube
      FABL.example3_19FreeCoordinates) :
  FABL.signValue
      (FABL.signRestriction
        FABL.example3_19Function
        FABL.example3_19FreeCoordinates
        FABL.example3_19FixedAssignment
        y) =
    -1 / 2 +
          1 / 2 *
            FABL.signValue
              (y FABL.example3_19First) +
        1 / 2 *
          FABL.signValue
            (y FABL.example3_19Second) +
      1 / 2 *
          FABL.signValue
            (y FABL.example3_19First) *
        FABL.signValue
          (y FABL.example3_19Second)

O'Donnell, Example 3.19, equation (3.4): the Fourier expansion after fixing
`x₃ = 1, x₄ = -1`.

theoremdefined in FABL/Chapter03/Restrictions.lean

complete

theorem FABL.example3_19_restrictionFourierCoeff_first :
  FABL.restrictionFourierCoeff FABL.example3_19Function.toReal
      FABL.example3_19FreeCoordinates {FABL.example3_19First}
      FABL.example3_19FixedAssignment =
    1 / 2

theorem FABL.example3_19_restrictionFourierCoeff_first :
  FABL.restrictionFourierCoeff
      FABL.example3_19Function.toReal
      FABL.example3_19FreeCoordinates
      {FABL.example3_19First}
      FABL.example3_19FixedAssignment =
    1 / 2

The first-coordinate Fourier coefficient of the concrete restriction in Example 3.19 is
`1 / 2`. This is the typed version of the coefficient computation following equation (3.4).

theoremdefined in FABL/Chapter03/Restrictions.lean

complete

theorem FABL.example3_19_first_coefficient_arithmetic :
  -1 / 8 + 1 / 8 + 3 / 8 + 1 / 8 = 1 / 2

theorem FABL.example3_19_first_coefficient_arithmetic :
  -1 / 8 + 1 / 8 + 3 / 8 + 1 / 8 = 1 / 2

The coefficient arithmetic at the end of Example 3.19.

Definition3.3.5

Statement uses 2

Statement dependency previews

Preview

Lemma 3.3.1

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

Used by 2

Reverse dependency previews

Preview

Proposition 3.3.6

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

Tagssection-3-3fidelity-exact

Definition 3.20. Let f:\{-1,1\}^n\to\mathbb R, let (J,\bar J) be a partition of [n], and let S\subseteq J. Define F_{S\mid J}f:\{-1,1\}^{\bar J}\to\mathbb R by F_{S\mid J}f(z)=\widehat{f_{J\mid z}}(S). When the partition is understood, one may write simply F_{S\mid}f.

Lean code for Definition3.3.5●1 definition

defdefined in FABL/Chapter03/Restrictions.lean

complete

def FABL.restrictionFourierCoeff {n : ℕ} (f : FABL.SignCube n → ℝ)
  (J : Finset (Fin n)) (S : Finset ↥J) : FABL.FixedSignCube J → ℝ

def FABL.restrictionFourierCoeff {n : ℕ}
  (f : FABL.SignCube n → ℝ)
  (J : Finset (Fin n)) (S : Finset ↥J) :
  FABL.FixedSignCube J → ℝ

O'Donnell, Definition 3.20: the coefficient on `S` after restriction, regarded as a
function of the complementary assignment `z`.

Proposition3.3.6

Statement uses 4

Statement dependency previews

Preview

Theorem 1.2.3

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 1✓L∃∀N

Tagssection-3-3fidelity-exact

Proposition 3.21. In the setting of Definition 3.20, for every z\in\{-1,1\}^{\bar J} one has the Fourier expansion F_{S\mid J}f(z) =\sum_{T\subseteq\bar J}\widehat f(S\cup T)z^T. Equivalently, for every T\subseteq\bar J, \widehat{F_{S\mid J}f}(T)=\widehat f(S\cup T).

Lean code for Proposition3.3.6●2 theorems

theoremdefined in FABL/Chapter03/Restrictions.lean

complete

theorem FABL.indexedFourierCoeff_restrictionFourierCoeff {n : ℕ}
  (f : FABL.SignCube n → ℝ) (J : Finset (Fin n)) (S : Finset ↥J)
  (T : Finset (FABL.FixedIndex J)) :
  FABL.indexedFourierCoeff (FABL.restrictionFourierCoeff f J S) T =
    FABL.fourierCoeff f
      (FABL.liftFreeFrequency S ∪ FABL.liftFixedFrequency T)

theorem FABL.indexedFourierCoeff_restrictionFourierCoeff
  {n : ℕ} (f : FABL.SignCube n → ℝ)
  (J : Finset (Fin n)) (S : Finset ↥J)
  (T : Finset (FABL.FixedIndex J)) :
  FABL.indexedFourierCoeff
      (FABL.restrictionFourierCoeff f J S)
      T =
    FABL.fourierCoeff f
      (FABL.liftFreeFrequency S ∪
        FABL.liftFixedFrequency T)

O'Donnell, Proposition 3.21: the Fourier coefficient on `T` of the function sending a
complementary assignment to the restricted coefficient on `S` is the original coefficient on
`S ∪ T`. The two lifts make the book's subtype-indexed union explicit.

theoremdefined in FABL/Chapter03/Restrictions.lean

complete

theorem FABL.restrictionFourierCoeff_eq_sum {n : ℕ} (f : FABL.SignCube n → ℝ)
  (J : Finset (Fin n)) (S : Finset ↥J) (z : FABL.FixedSignCube J) :
  FABL.restrictionFourierCoeff f J S z =
    ∑ T,
      FABL.fourierCoeff f
          (FABL.liftFreeFrequency S ∪ FABL.liftFixedFrequency T) *
        FABL.indexedMonomial T z

theorem FABL.restrictionFourierCoeff_eq_sum
  {n : ℕ} (f : FABL.SignCube n → ℝ)
  (J : Finset (Fin n)) (S : Finset ↥J)
  (z : FABL.FixedSignCube J) :
  FABL.restrictionFourierCoeff f J S z =
    ∑ T,
      FABL.fourierCoeff f
          (FABL.liftFreeFrequency S ∪
            FABL.liftFixedFrequency T) *
        FABL.indexedMonomial T z

The Fourier-expansion form of O'Donnell, Proposition 3.21.

Corollary3.3.7

Statement uses 4

Statement dependency previews

Preview

Theorem 1.4.2

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 1✓L∃∀N

Tagssection-3-3fidelity-exact

Corollary 3.22. Let f:\{-1,1\}^n\to\mathbb R, let (J,\bar J) be a partition of [n], and fix S\subseteq J. If \boldsymbol z\sim\{-1,1\}^{\bar J} is chosen uniformly at random, then \mathbb E_{\boldsymbol z}[\widehat{f_{J\mid\boldsymbol z}}(S)]=\widehat f(S), and \mathbb E_{\boldsymbol z} \left[\widehat{f_{J\mid\boldsymbol z}}(S)^2\right] =\sum_{T\subseteq\bar J}\widehat f(S\cup T)^2.

Lean code for Corollary3.3.7●2 theorems

theoremdefined in FABL/Chapter03/Restrictions.lean

complete

theorem FABL.expect_restrictionFourierCoeff {n : ℕ} (f : FABL.SignCube n → ℝ)
  (J : Finset (Fin n)) (S : Finset ↥J) :
  (Finset.univ.expect fun z => FABL.restrictionFourierCoeff f J S z) =
    FABL.fourierCoeff f (FABL.liftFreeFrequency S)

theorem FABL.expect_restrictionFourierCoeff
  {n : ℕ} (f : FABL.SignCube n → ℝ)
  (J : Finset (Fin n)) (S : Finset ↥J) :
  (Finset.univ.expect fun z =>
      FABL.restrictionFourierCoeff f J S
        z) =
    FABL.fourierCoeff f
      (FABL.liftFreeFrequency S)

The first-moment identity in O'Donnell, Corollary 3.22.

theoremdefined in FABL/Chapter03/Restrictions.lean

complete

theorem FABL.expect_sq_restrictionFourierCoeff {n : ℕ} (f : FABL.SignCube n → ℝ)
  (J : Finset (Fin n)) (S : Finset ↥J) :
  (Finset.univ.expect fun z =>
      FABL.restrictionFourierCoeff f J S z ^ 2) =
    ∑ T,
      FABL.fourierCoeff f
          (FABL.liftFreeFrequency S ∪ FABL.liftFixedFrequency T) ^
        2

theorem FABL.expect_sq_restrictionFourierCoeff
  {n : ℕ} (f : FABL.SignCube n → ℝ)
  (J : Finset (Fin n)) (S : Finset ↥J) :
  (Finset.univ.expect fun z =>
      FABL.restrictionFourierCoeff f J S
          z ^
        2) =
    ∑ T,
      FABL.fourierCoeff f
          (FABL.liftFreeFrequency S ∪
            FABL.liftFixedFrequency T) ^
        2

The second-moment identity in O'Donnell, Corollary 3.22.

Definition3.3.8

uses 1used by 1✓L∃∀N

Tagssection-3-3fidelity-exact

Definition 3.23. If f:\mathbb F_2^n\to\mathbb R and H\le\mathbb F_2^n is a linear subspace, write f_H:H\to\mathbb R for the restriction of f to H; thus f_H(h)=f(h) for every h\in H.

Lean code for Definition3.3.8●1 definition

defdefined in FABL/Chapter03/Restrictions.lean

complete

def FABL.subspaceRestriction.{u_1} {n : ℕ} {α : Type u_1}
  (f : FABL.F₂Cube n → α) (H : Submodule FABL.𝔽₂ (FABL.F₂Cube n)) :
  ↥H → α

def FABL.subspaceRestriction.{u_1} {n : ℕ}
  {α : Type u_1} (f : FABL.F₂Cube n → α)
  (H :
    Submodule FABL.𝔽₂ (FABL.F₂Cube n)) :
  ↥H → α

O'Donnell, Definition 3.23, conservatively generalized in the codomain: the restriction of
`f` to the binary subspace `H`.

Definition3.3.9

uses 1

Used by 2

Reverse dependency previews

Preview

Lemma 3.3.10

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

Tagssection-3-3fidelity-exact

Definition 3.24. Let f:\mathbb F_2^n\to\mathbb R and z\in\mathbb F_2^n. Define f^{+z}:\mathbb F_2^n\to\mathbb R by f^{+z}(x)=f(x+z).

Lean code for Definition3.3.9●1 definition

defdefined in FABL/Chapter03/Restrictions.lean

complete

def FABL.domainTranslate.{u_1} {n : ℕ} {α : Type u_1}
  (f : FABL.F₂Cube n → α) (z : FABL.F₂Cube n) : FABL.F₂Cube n → α

def FABL.domainTranslate.{u_1} {n : ℕ}
  {α : Type u_1} (f : FABL.F₂Cube n → α)
  (z : FABL.F₂Cube n) : FABL.F₂Cube n → α

O'Donnell, Definition 3.24, conservatively generalized in the codomain: translation of the
domain by `z`.

Lemma3.3.10

Statement uses 3

Statement dependency previews

Preview

Lemma 1.2.7

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 1✓L∃∀N

Tagssection-3-3fidelity-exact

Fact 3.25. For every \gamma\in\widehat{\mathbb F_2^n}, the Fourier coefficient of f^{+z} is \widehat{f^{+z}}(\gamma) =(-1)^{\gamma\cdot z}\widehat f(\gamma) =\chi_\gamma(z)\widehat f(\gamma). Equivalently, f^{+z}(x) =\sum_{\gamma\in\widehat{\mathbb F_2^n}} \chi_\gamma(z)\widehat f(\gamma)\chi_\gamma(x). Here the dual group \widehat{\mathbb F_2^n} is identified with \mathbb F_2^n through the dot product.

Lean code for Lemma3.3.10●3 theorems

theoremdefined in FABL/Chapter03/Restrictions.lean

complete

theorem FABL.vectorFourierCoeff_domainTranslate {n : ℕ} (f : FABL.F₂Cube n → ℝ)
  (z γ : FABL.F₂Cube n) :
  FABL.vectorFourierCoeff (FABL.domainTranslate f z) γ =
    (FABL.vectorWalshCharacter γ) z * FABL.vectorFourierCoeff f γ

theorem FABL.vectorFourierCoeff_domainTranslate
  {n : ℕ} (f : FABL.F₂Cube n → ℝ)
  (z γ : FABL.F₂Cube n) :
  FABL.vectorFourierCoeff
      (FABL.domainTranslate f z) γ =
    (FABL.vectorWalshCharacter γ) z *
      FABL.vectorFourierCoeff f γ

O'Donnell, Fact 3.25: translating the domain multiplies a Fourier coefficient by the
corresponding Walsh character evaluated at the translation vector.

theoremdefined in FABL/Chapter03/Restrictions.lean

complete

theorem FABL.vectorFourierCoeff_domainTranslate_eq_binarySign {n : ℕ}
  (f : FABL.F₂Cube n → ℝ) (z γ : FABL.F₂Cube n) :
  FABL.vectorFourierCoeff (FABL.domainTranslate f z) γ =
    FABL.binarySign (FABL.f₂DotProduct γ z) *
      FABL.vectorFourierCoeff f γ

theorem FABL.vectorFourierCoeff_domainTranslate_eq_binarySign
  {n : ℕ} (f : FABL.F₂Cube n → ℝ)
  (z γ : FABL.F₂Cube n) :
  FABL.vectorFourierCoeff
      (FABL.domainTranslate f z) γ =
    FABL.binarySign
        (FABL.f₂DotProduct γ z) *
      FABL.vectorFourierCoeff f γ

The dot-product form of the coefficient identity in O'Donnell, Fact 3.25.

theoremdefined in FABL/Chapter03/Restrictions.lean

complete

theorem FABL.domainTranslate_fourier_expansion {n : ℕ} (f : FABL.F₂Cube n → ℝ)
  (z x : FABL.F₂Cube n) :
  FABL.domainTranslate f z x =
    ∑ γ,
      (FABL.vectorWalshCharacter γ) z * FABL.vectorFourierCoeff f γ *
        (FABL.vectorWalshCharacter γ) x

theorem FABL.domainTranslate_fourier_expansion
  {n : ℕ} (f : FABL.F₂Cube n → ℝ)
  (z x : FABL.F₂Cube n) :
  FABL.domainTranslate f z x =
    ∑ γ,
      (FABL.vectorWalshCharacter γ) z *
          FABL.vectorFourierCoeff f γ *
        (FABL.vectorWalshCharacter γ) x

The Fourier-expansion form of O'Donnell, Fact 3.25.

Definition3.3.11

Statement uses 3

Statement dependency previews

Preview

Lemma 3.2.7

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 1✓L∃∀N

Tagssection-3-3fidelity-exact

Definition 3.26. Let f:\mathbb F_2^n\to\mathbb R, z\in\mathbb F_2^n, and H\le\mathbb F_2^n. Write f_H^{+z}:H\to\mathbb R for the function (f^{+z})_H; equivalently, f_H^{+z}(h)=f(h+z) for h\in H. This is the restriction of f to the coset H+z, with the representative z made explicit.

Lean code for Definition3.3.11●1 definition

defdefined in FABL/Chapter03/Restrictions.lean

complete

def FABL.affineSubspaceRestriction.{u_1} {n : ℕ} {α : Type u_1}
  (f : FABL.F₂Cube n → α) (H : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (z : FABL.F₂Cube n) : ↥H → α

def FABL.affineSubspaceRestriction.{u_1}
  {n : ℕ} {α : Type u_1}
  (f : FABL.F₂Cube n → α)
  (H : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (z : FABL.F₂Cube n) : ↥H → α

O'Donnell, Definition 3.26, conservatively generalized in the codomain: restriction to the
coset `H + z`, with the representative `z` kept explicit.

Lemma3.3.12

Statement uses 3

Statement dependency previews

Preview

Lemma 1.5.2

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 1✓L∃∀N

Tagssection-3-3supportfidelity-exact

Average on an affine subspace. Let f:\mathbb F_2^n\to\mathbb R, H\le\mathbb F_2^n, and z\in\mathbb F_2^n. The Fourier coefficient of f_H^{+z} at the trivial character is its uniform average on H, and this average is the density-weighted inner product on the ambient cube: \widehat{f_H^{+z}}(0) =\mathbb E_{\boldsymbol h\sim H}[f(\boldsymbol h+z)] =\langle\varphi_H,f^{+z}\rangle.

Lean code for Lemma3.3.12●6 declarations

defdefined in FABL/Chapter03/Restrictions.lean

complete

def FABL.finiteAddFourierCoeff.{u_1} {G : Type u_1} [Fintype G]
  [AddCommGroup G] (g : G → ℝ) (ψ : AddChar G ℝ) : ℝ

def FABL.finiteAddFourierCoeff.{u_1}
  {G : Type u_1} [Fintype G]
  [AddCommGroup G] (g : G → ℝ)
  (ψ : AddChar G ℝ) : ℝ

The normalized Fourier coefficient of a function on a finite additive commutative group,
indexed by an additive character.

theoremdefined in FABL/Chapter03/Restrictions.lean

complete

theorem FABL.finiteAddFourierCoeff_zero_eq_expect.{u_1} {G : Type u_1}
  [Fintype G] [AddCommGroup G] (g : G → ℝ) :
  FABL.finiteAddFourierCoeff g 0 = Finset.univ.expect fun x => g x

theorem FABL.finiteAddFourierCoeff_zero_eq_expect.{u_1}
  {G : Type u_1} [Fintype G]
  [AddCommGroup G] (g : G → ℝ) :
  FABL.finiteAddFourierCoeff g 0 =
    Finset.univ.expect fun x => g x

The coefficient at the trivial additive character is the uniform expectation.

theoremdefined in FABL/Chapter03/Restrictions.lean

complete

theorem FABL.finiteAddFourierCoeff_affineSubspaceRestriction_zero_eq_expect
  {n : ℕ} (f : FABL.F₂Cube n → ℝ)
  (H : Submodule FABL.𝔽₂ (FABL.F₂Cube n)) (z : FABL.F₂Cube n) :
  FABL.finiteAddFourierCoeff (FABL.affineSubspaceRestriction f H z) 0 =
    Finset.univ.expect fun h => f (↑h + z)

theorem FABL.finiteAddFourierCoeff_affineSubspaceRestriction_zero_eq_expect
  {n : ℕ} (f : FABL.F₂Cube n → ℝ)
  (H : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (z : FABL.F₂Cube n) :
  FABL.finiteAddFourierCoeff
      (FABL.affineSubspaceRestriction f H
        z)
      0 =
    Finset.univ.expect fun h => f (↑h + z)

The Fourier coefficient at the trivial character of an affine-subspace restriction is its
uniform average.

theoremdefined in FABL/Chapter03/Restrictions.lean

complete

theorem FABL.expect_vectorWalshCharacter_submodule {n : ℕ}
  (H : Submodule FABL.𝔽₂ (FABL.F₂Cube n)) (γ : FABL.F₂Cube n) :
  (Finset.univ.expect fun h => (FABL.vectorWalshCharacter γ) ↑h) =
    if γ ∈ FABL.perpendicularSubspace H then 1 else 0

theorem FABL.expect_vectorWalshCharacter_submodule
  {n : ℕ}
  (H : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (γ : FABL.F₂Cube n) :
  (Finset.univ.expect fun h =>
      (FABL.vectorWalshCharacter γ) ↑h) =
    if
        γ ∈
          FABL.perpendicularSubspace
            H then
      1
    else 0

A vector-indexed Walsh character averaged over `H` is one precisely when its index lies in
`Hᵖ`, and is zero otherwise.

theoremdefined in FABL/Chapter03/Restrictions.lean

complete

theorem FABL.uniformInner_subsetDensity_domainTranslate_eq_sum {n : ℕ}
  (f : FABL.F₂Cube n → ℝ) (H : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (z : FABL.F₂Cube n) :
  FABL.uniformInner (FABL.subsetDensity ↑H ⋯).toFun
      (FABL.domainTranslate f z) =
    ∑ γ, (FABL.vectorWalshCharacter ↑γ) z * FABL.vectorFourierCoeff f ↑γ

theorem FABL.uniformInner_subsetDensity_domainTranslate_eq_sum
  {n : ℕ} (f : FABL.F₂Cube n → ℝ)
  (H : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (z : FABL.F₂Cube n) :
  FABL.uniformInner
      (FABL.subsetDensity ↑H ⋯).toFun
      (FABL.domainTranslate f z) =
    ∑ γ,
      (FABL.vectorWalshCharacter ↑γ) z *
        FABL.vectorFourierCoeff f ↑γ

The uniform inner product of the density of `H` with a translated function is the Fourier
sum over `Hᵖ`. This is the Plancherel calculation immediately preceding the Poisson Summation
Formula.

theoremdefined in FABL/Chapter03/Restrictions.lean

complete

theorem FABL.expect_affineSubspaceRestriction_eq_uniformInner {n : ℕ}
  (f : FABL.F₂Cube n → ℝ) (H : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (z : FABL.F₂Cube n) :
  (Finset.univ.expect fun h => FABL.affineSubspaceRestriction f H z h) =
    FABL.uniformInner (FABL.subsetDensity ↑H ⋯).toFun
      (FABL.domainTranslate f z)

theorem FABL.expect_affineSubspaceRestriction_eq_uniformInner
  {n : ℕ} (f : FABL.F₂Cube n → ℝ)
  (H : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (z : FABL.F₂Cube n) :
  (Finset.univ.expect fun h =>
      FABL.affineSubspaceRestriction f H z
        h) =
    FABL.uniformInner
      (FABL.subsetDensity ↑H ⋯).toFun
      (FABL.domainTranslate f z)

The average value of `f` on `H + z` is the uniform inner product of the density of `H`
with the translated function, as stated immediately before the Poisson Summation Formula.

Theorem3.3.13

Statement uses 5

Statement dependency previews

Preview

Theorem 1.4.3

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 0✓L∃∀N

Tagssection-3-3fidelity-exact

Poisson Summation Formula. Let f:\mathbb F_2^n\to\mathbb R, H\le\mathbb F_2^n, and z\in\mathbb F_2^n. Then \mathbb E_{\boldsymbol h\sim H}[f(\boldsymbol h+z)] =\sum_{\gamma\in H^\perp}\chi_\gamma(z)\widehat f(\gamma), where H^\perp =\left\{\gamma\in\widehat{\mathbb F_2^n}: \gamma\cdot h=0\ \text{for every }h\in H\right\}.

Lean code for Theorem3.3.13●2 theorems

theoremdefined in FABL/Chapter03/Restrictions.lean

complete

theorem FABL.expect_affineSubspaceRestriction_eq_sum {n : ℕ}
  (f : FABL.F₂Cube n → ℝ) (H : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (z : FABL.F₂Cube n) :
  (Finset.univ.expect fun h => FABL.affineSubspaceRestriction f H z h) =
    ∑ γ, (FABL.vectorWalshCharacter ↑γ) z * FABL.vectorFourierCoeff f ↑γ

theorem FABL.expect_affineSubspaceRestriction_eq_sum
  {n : ℕ} (f : FABL.F₂Cube n → ℝ)
  (H : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (z : FABL.F₂Cube n) :
  (Finset.univ.expect fun h =>
      FABL.affineSubspaceRestriction f H z
        h) =
    ∑ γ,
      (FABL.vectorWalshCharacter ↑γ) z *
        FABL.vectorFourierCoeff f ↑γ

The direct finite-character calculation of the average of `f` on the coset `H + z`.

theoremdefined in FABL/Chapter03/Restrictions.lean

complete

theorem FABL.poissonSummationFormula {n : ℕ} (f : FABL.F₂Cube n → ℝ)
  (H : Submodule FABL.𝔽₂ (FABL.F₂Cube n)) (z : FABL.F₂Cube n) :
  (Finset.univ.expect fun h => f (↑h + z)) =
    ∑ γ, (FABL.vectorWalshCharacter ↑γ) z * FABL.vectorFourierCoeff f ↑γ

theorem FABL.poissonSummationFormula {n : ℕ}
  (f : FABL.F₂Cube n → ℝ)
  (H : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (z : FABL.F₂Cube n) :
  (Finset.univ.expect fun h =>
      f (↑h + z)) =
    ∑ γ,
      (FABL.vectorWalshCharacter ↑γ) z *
        FABL.vectorFourierCoeff f ↑γ

O'Donnell's Poisson Summation Formula on the binary cube.