FourierWeights.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

def OAI.TalagrandDiscreteConvexity.correction line 12
Source documentation
The alternating factor for a coordinate inside the differentiated set.
```
def correction (q : ℝ) (bit : Bool) : ℝ :=
…
```
theorem OAI.TalagrandDiscreteConvexity.correction_false line 15
theorem OAI.TalagrandDiscreteConvexity.correction_true line 17
def OAI.TalagrandDiscreteConvexity.rowKernel line 22
Source documentation
Coordinate product defining the alternating partial expectation.
```
def rowKernel (q : ℝ) (U : Finset V) (x : V → Bool) : ℝ :=
…
```
def OAI.TalagrandDiscreteConvexity.b line 27
Source documentation
Exactly (1-q)^|U| times the alternating sum over the coordinates in U, with independent Bernoulli expectation on its complement.
```
def b (q : ℝ) (f : (V → Bool) → ℝ) (U : Finset V) : ℝ :=
…
```
def OAI.TalagrandDiscreteConvexity.w line 31
Source documentation
The nonnegative weights used by both global and exceptional-set bounds.
```
def w (q : ℝ) (f : (V → Bool) → ℝ) (U : Finset V) : ℝ :=
…
```
theorem OAI.TalagrandDiscreteConvexity.rowKernel_eq_alternating_product line 35
Source documentation
Separate the alternating coordinates from the independent outside mass.
```
theorem rowKernel_eq_alternating_product (q : ℝ) (U : Finset V) (x : V → Bool) :
    rowKernel q U x = (1 - q) ^ U.card *
      (∏ i ∈ U, if x i then (-1 : ℝ) else 1) *
      ∏ i ∈ Finset.univ \ U, bitWeight q (x i) := by
…
```
Mentions: OAI.TalagrandDiscreteConvexity.rowKernel, OAI.TalagrandDiscreteConvexity.bitWeight

theorem OAI.TalagrandDiscreteConvexity.b_eq_alternating_sum line 57

Source documentation

The explicit alternating partial-expectation formula for the coefficient.

theorem b_eq_alternating_sum (q : ℝ) (f : (V → Bool) → ℝ) (U : Finset V) :
    b q f U = (1 - q) ^ U.card *
      ∑ x, f x * (∏ i ∈ U, if x i then (-1 : ℝ) else 1) *
        ∏ i ∈ Finset.univ \ U, bitWeight q (x i) := by
…

Mentions: OAI.TalagrandDiscreteConvexity.b, OAI.TalagrandDiscreteConvexity.bitWeight

theorem OAI.TalagrandDiscreteConvexity.rowKernel_empty line 66
theorem OAI.TalagrandDiscreteConvexity.b_empty line 71
Source documentation
The empty coefficient is the original biased expectation.
```
@[simp] theorem b_empty (q : ℝ) (f : (V → Bool) → ℝ) :
    b q f ∅ = cubeExpectation q f := by
…
```
Mentions: OAI.TalagrandDiscreteConvexity.b, OAI.TalagrandDiscreteConvexity.cubeExpectation
theorem OAI.TalagrandDiscreteConvexity.w_nonneg line 78