Mixed moments of independently sampled balanced predicates
Lax253009.MixedPredicateMoments · concepts/Lax253009/MixedPredicateMoments.lean · lax-253009
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Theorem
For a fixed tuple of supports with union of size , the absolute mixed moment is at most . Here is the number of supports and is the size of the predicate domain. This is a normalized version of Lemma 4.12, with a nonoptimal concentration factor. Condition on all but one predicate in each nonempty subcollection; a union bound controls their correlations simultaneously. Independence of the coordinate labels then gives one factor per point of the union.
Concept map
Evidence
Each proof establishes this claim relative to its assumptions.
Lean source view on GitHub
| 1 | import Lax253009.BalancedPredicates |
| 2 | import Lax253009.HigherMoments |
| 3 | |
| 4 | /-! |
| 5 | --- |
| 6 | title: Mixed moments of independently sampled balanced predicates |
| 7 | type: theorem |
| 8 | --- |
| 9 | For a fixed tuple of supports with union of size , the absolute mixed |
| 10 | moment is at most . Here is the number |
| 11 | of supports and is the size of the predicate domain. This is a |
| 12 | normalized version of Lemma 4.12, with a nonoptimal concentration factor. |
| 13 | Condition on all but one predicate in each nonempty subcollection; a |
| 14 | union bound controls their correlations simultaneously. Independence of |
| 15 | the coordinate labels then gives one factor per point of the union. |
| 16 | -/ |
| 17 | |
| 18 | namespace Lax253009.MixedPredicateMoments |
| 19 | |
| 20 | open BooleanFourier BalancedPredicates |
| 21 | open scoped BigOperators |
| 22 | |
| 23 | axiom bound {ι κ : Type} [Fintype ι] [DecidableEq ι] |
| 24 | [Fintype κ] [DecidableEq κ] [Nonempty κ] |
| 25 | (n : ℕ) (hn : 0 < n) (hN : Fintype.card κ = 2 * n) |
| 26 | (m : ℕ) (S : Fin m → Finset ι) (q : ℝ) (hq : 0 ≤ q) : |
| 27 | |𝔼 B : Fin m → predicates κ n, 𝔼 f : ι → κ, |
| 28 | ∏ j, ∏ i ∈ S j, sign ((B j).val (f i))| ≤ |
| 29 | q ^ (Finset.univ.biUnion S).card + (2 : ℝ) ^ m * |
| 30 | (2 * (Fintype.card κ + 1 : ℝ) * Real.exp (-(Fintype.card κ : ℝ) * q ^ 2 / 2)) |
| 31 | |
| 32 | end Lax253009.MixedPredicateMoments |
| 33 |
From Mathlib
none
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments