FourierProductKernel.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Orthogonality of the biased product kernel

The two possible choices at one coordinate give its Bernoulli diagonal matrix. Summing over all subsets tensors this identity, with no square roots or choice of a normalized Fourier basis.

theorem OAI.TalagrandDiscreteConvexity.bitWeight_correction_gram line 22
Source documentation
The one-coordinate Gram identity for the mass and alternating factors.
```
theorem bitWeight_correction_gram (q : ℝ) (hq1 : q < 1) (x y : Bool) :
    bitWeight q x * bitWeight q y +
        (q / (1 - q)) * correction q x * correction q y =
      if x = y then bitWeight q x else 0 := by
…
```
Mentions: OAI.TalagrandDiscreteConvexity.bitWeight, OAI.TalagrandDiscreteConvexity.correction

theorem OAI.TalagrandDiscreteConvexity.rowKernel_weighted_product line 33

Source documentation

Move the subset weight into the coordinate product.

theorem rowKernel_weighted_product (q : ℝ) (U : Finset V) (x y : V → Bool) :
    (q / (1 - q)) ^ U.card * rowKernel q U x * rowKernel q U y =
      ∏ i, if i ∈ U then
        (q / (1 - q)) * correction q (x i) * correction q (y i)
      else bitWeight q (x i) * bitWeight q (y i) := by
…

Mentions: OAI.TalagrandDiscreteConvexity.rowKernel, OAI.TalagrandDiscreteConvexity.correction, OAI.TalagrandDiscreteConvexity.bitWeight

theorem OAI.TalagrandDiscreteConvexity.rowKernel_gram line 51
Source documentation
Summing the weighted kernel products over all subsets gives the original Bernoulli mass on the diagonal and zero away from the diagonal.
```
theorem rowKernel_gram (q : ℝ) (_hq0 : 0 < q) (hq1 : q < 1) (x y : V → Bool) :
    (∑ U : Finset V,
      (q / (1 - q)) ^ U.card * rowKernel q U x * rowKernel q U y) =
      if x = y then cubeWeight q x else 0 := by
…
```
Mentions: OAI.TalagrandDiscreteConvexity.rowKernel, OAI.TalagrandDiscreteConvexity.cubeWeight