FourierOption.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem313.BiasedFourier.optionFinsetEquiv line 16
Source documentation
Separate Fourier supports according to whether the distinguished coordinate occurs.
```
def optionFinsetEquiv : Finset (Option ι) ≃ Finset ι ⊕ Finset ι := by
…
```
theorem OAI.Problem313.BiasedFourier.sum_option_finset line 30
theorem OAI.Problem313.BiasedFourier.char_map_some line 39
theorem OAI.Problem313.BiasedFourier.char_insertNone line 45

theorem OAI.Problem313.BiasedFourier.synthesis_option line 52

Source documentation

A noise-weighted Fourier polynomial separates into its two first-coordinate pieces.

theorem synthesis_option (p ρ : ℝ) (c : Finset (Option ι) → ℝ)
    (x : Option ι → Bool) :
    (∑ S, ρ ^ S.card * c S * char p S x) =
      (∑ S : Finset ι, ρ ^ S.card * c (S.map Function.Embedding.some) *
        char p S (fun i => x (some i))) +
      ρ * chi p (x none) *
        ∑ S : Finset ι, ρ ^ S.card * c (Finset.insertNone S) *
          char p S (fun i => x (some i)) := by
…

Mentions: OAI.Problem313.BiasedFourier.char, OAI.Problem313.BiasedFourier.chi

theorem OAI.Problem313.BiasedFourier.coefficient_energy_option line 70