OAI/Combinatorics/SharpThreshold/FourierOptionExpectation.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem313.BiasedFourier.weight_option line 17

   Source documentation

   Separate the new coordinate from the product Bernoulli weight.

   theorem weight_option (p : ℝ) (x : Option ι → Bool) :
       weight p x = scalarWeight p (x none) * weight p (fun i => x (some i)) := by
   …

   Mentions: OAI.Problem313.BiasedFourier.weight, OAI.Problem313.BiasedFourier.scalarWeight

2. theorem OAI.Problem313.BiasedFourier.weight_option_elim line 21
3. theorem OAI.Problem313.BiasedFourier.weighted_sum_option line 28

   Source documentation

   Exact expectation splitting at the distinguished none coordinate. This identity is polynomial and requires no restriction on the bias.

   theorem weighted_sum_option (p : ℝ) (g : (Option ι → Bool) → ℝ) :
       (∑ x, weight p x * g x) =
         (1 - p) * (∑ y, weight p y * g ((fun i : Option ι => Option.elim i false y))) +
           p * (∑ y, weight p y * g ((fun i : Option ι => Option.elim i true y))) := by
   …

   Mentions: OAI.Problem313.BiasedFourier.weight