FourierRestriction.lean`

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem313.BiasedFourier.coeff_restricted_coeff line 17
Source documentation
Fourier transformation in the exterior variables of a conditional Fourier coefficient recovers the full Fourier coefficient on the disjoint support.
```
theorem coeff_restricted_coeff (p : ℝ) (f : (ι ⊕ κ → Bool) → ℝ)
    (A : Finset ι) (D : Finset κ) :
    coeff p (fun y => coeff p (fun x => f (Sum.elim x y)) A) D =
      coeff p f (A.disjSum D) := by
…
```
Mentions: OAI.Problem313.BiasedFourier.coeff
theorem OAI.Problem313.BiasedFourier.restricted_coeff_expansion line 58
Source documentation
A conditional Fourier coefficient expands in the exterior characters, with full Fourier coefficients and no cutoff on the exterior degree.
```
theorem restricted_coeff_expansion {p : ℝ} (hp : 0 < p) (hp1 : p < 1)
    (f : (ι ⊕ κ → Bool) → ℝ) (A : Finset ι) (y : κ → Bool) :
    coeff p (fun x => f (Sum.elim x y)) A =
      ∑ D : Finset κ, coeff p f (A.disjSum D) * char p D y := by
…
```
Mentions: OAI.Problem313.BiasedFourier.coeff, OAI.Problem313.BiasedFourier.char
theorem OAI.Problem313.BiasedFourier.restricted_coeff_sq_average line 69
Source documentation
Averaging the square of a conditional coefficient retains all exterior Fourier degrees. This is the single-coefficient restriction identity.
```
theorem restricted_coeff_sq_average [DecidableEq κ] {p : ℝ} (hp : 0 < p) (hp1 : p < 1)
    (f : (ι ⊕ κ → Bool) → ℝ) (A : Finset ι) :
    (∑ y : κ → Bool, weight p y *
      (coeff p (fun x => f (Sum.elim x y)) A) ^ 2) =
      ∑ D : Finset κ, (coeff p f (A.disjSum D)) ^ 2 := by
…
```
Mentions: OAI.Problem313.BiasedFourier.weight, OAI.Problem313.BiasedFourier.coeff