FourierGlobalBound.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Biased Parseval and the global weight bound

The exact Parseval multiplier for the unnormalized coefficients is (q / (1-q))^|U|. The desired multiplier q^|U| is smaller for 0 < q < 1. The actual product-kernel identity proves Parseval here; it is not a hypothesis of the global bound or its family-indicator specialization.

theorem OAI.TalagrandDiscreteConvexity.biased_parseval line 25
Source documentation
Square-root-free biased Parseval for the actual alternating coefficients.
```
theorem biased_parseval (q : ℝ) (hq0 : 0 < q) (hq1 : q < 1)
    (f : (V → Bool) → ℝ) :
    (∑ U : Finset V, (q / (1 - q)) ^ U.card * w q f U) =
      cubeExpectation q (fun x => (f x) ^ 2) := by
…
```
Mentions: OAI.TalagrandDiscreteConvexity.w, OAI.TalagrandDiscreteConvexity.cubeExpectation
theorem OAI.TalagrandDiscreteConvexity.weight_sum_le_second_moment line 34

theorem OAI.TalagrandDiscreteConvexity.global_weight_bound line 48

Source documentation

A bounded-square function has global weight sum at most one.

theorem global_weight_bound (q : ℝ) (hq0 : 0 < q) (hq1 : q < 1)
    (f : (V → Bool) → ℝ) (hf : ∀ x, (f x) ^ 2 ≤ 1) :
    (∑ U : Finset V, q ^ U.card * w q f U) ≤ 1 := by
…

Mentions: OAI.TalagrandDiscreteConvexity.w

theorem OAI.TalagrandDiscreteConvexity.indicator_global_weight_bound line 64
Source documentation
The global weight bound for the actual indicator of an arbitrary family. No monotonicity or density assumption on the family is needed.
```
theorem indicator_global_weight_bound (q : ℝ) (hq0 : 0 < q) (hq1 : q < 1)
    (D : Family V) :
    (∑ U : Finset V, q ^ U.card * w q (familyIndicator D) U) ≤ 1 := by
…
```
Mentions: OAI.TalagrandDiscreteConvexity.Family, OAI.TalagrandDiscreteConvexity.w, OAI.TalagrandDiscreteConvexity.familyIndicator