FourierProjection.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem313.BiasedFourier.project line 19
Source documentation
The projection onto the specified finite collection of Fourier characters.
```
def project (p : ℝ) (L : Finset (Finset ι))
    (g : (ι → Bool) → ℝ) (x : ι → Bool) : ℝ :=
…
```
theorem OAI.Problem313.BiasedFourier.project_inner line 24
Source documentation
Pairing a function with its projection gives its selected Fourier energy.
```
theorem project_inner (p : ℝ) (L : Finset (Finset ι)) (g : (ι → Bool) → ℝ) :
    (∑ x, weight p x * g x * project p L g x) =
      ∑ S ∈ L, (coeff p g S) ^ 2 := by
…
```
Mentions: OAI.Problem313.BiasedFourier.weight, OAI.Problem313.BiasedFourier.project, OAI.Problem313.BiasedFourier.coeff
theorem OAI.Problem313.BiasedFourier.project_second_moment line 45
Source documentation
The squared norm of a Fourier projection is its selected Fourier energy.
```
theorem project_second_moment {p : ℝ} (hp : 0 < p) (hp1 : p < 1)
    (L : Finset (Finset ι)) (g : (ι → Bool) → ℝ) :
    (∑ x, weight p x * (project p L g x) ^ 2) =
      ∑ S ∈ L, (coeff p g S) ^ 2 := by
…
```
Mentions: OAI.Problem313.BiasedFourier.weight, OAI.Problem313.BiasedFourier.project, OAI.Problem313.BiasedFourier.coeff
theorem OAI.Problem313.BiasedFourier.project_inner_eq_second_moment line 55
Source documentation
The defining orthogonality identity needed by the projection/Hölder estimate.
```
theorem project_inner_eq_second_moment {p : ℝ} (hp : 0 < p) (hp1 : p < 1)
    (L : Finset (Finset ι)) (g : (ι → Bool) → ℝ) :
    (∑ x, weight p x * g x * project p L g x) =
      ∑ x, weight p x * (project p L g x) ^ 2 := by
…
```
Mentions: OAI.Problem313.BiasedFourier.weight, OAI.Problem313.BiasedFourier.project

theorem OAI.Problem313.BiasedFourier.project_fourth_moment_of_noise line 63

Source documentation

Specialization of inverse-noise hypercontractivity to the canonical Fourier projection. The hypothesis is precisely the coefficient-form noise estimate.

theorem project_fourth_moment_of_noise (p rho k : ℝ)
    (hrho : 0 < rho) (hrho1 : rho ≤ 1)
    (hnoise : ∀ a : Finset ι → ℝ,
      (∑ x, weight p x *
        (∑ S, rho ^ S.card * a S * char p S x) ^ 4) ≤
          (∑ S, (a S) ^ 2) ^ 2)
    (L : Finset (Finset ι)) (g : (ι → Bool) → ℝ)
    (hdegree : ∀ S ∈ L, (S.card : ℝ) ≤ k) :
    (∑ x, weight p x * (project p L g x) ^ 4) ≤
      rho ^ (-4 * k) * (∑ S ∈ L, (coeff p g S) ^ 2) ^ 2 := by
…

Mentions: OAI.Problem313.BiasedFourier.weight, OAI.Problem313.BiasedFourier.char, OAI.Problem313.BiasedFourier.project, OAI.Problem313.BiasedFourier.coeff

theorem OAI.Problem313.BiasedFourier.project_energy_le_of_noise line 96

Source documentation

The concrete Fourier projection estimate for ternary-valued functions, including Boolean coordinate differences.

theorem project_energy_le_of_noise {p : ℝ} (hp : 0 < p) (hp1 : p < 1)
    (rho k : ℝ) (hrho : 0 < rho) (hrho1 : rho ≤ 1)
    (hnoise : ∀ a : Finset ι → ℝ,
      (∑ x, weight p x *
        (∑ S, rho ^ S.card * a S * char p S x) ^ 4) ≤
          (∑ S, (a S) ^ 2) ^ 2)
    (L : Finset (Finset ι)) (g : (ι → Bool) → ℝ)
    (hg : ∀ x, g x = -1 ∨ g x = 0 ∨ g x = 1)
    (hdegree : ∀ S ∈ L, (S.card : ℝ) ≤ k) :
    (∑ S ∈ L, (coeff p g S) ^ 2) ≤
      rho ^ (-2 * k) *
        (∑ x, if g x ≠ 0 then weight p x else 0) ^ (3 / 2 : ℝ) := by
…

Mentions: OAI.Problem313.BiasedFourier.weight, OAI.Problem313.BiasedFourier.char, OAI.Problem313.BiasedFourier.coeff