Higher-moment bound for the small-coefficient CNA term
Lax253009.SmallCoefficientSoundness · concepts/Lax253009/SmallCoefficientSoundness.lean · lax-253009
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Theorem
For coefficients of degree at most , squared mass at most one, and absolute value at most , split the mixed-moment expansion according to the union size of its double covers. Small unions contribute the bounds from Lemma 4.16; unions of size at least contribute at most the total double-cover weight times the mixed-correlation bound. This gives the normalized higher-moment estimate underlying Lemma 4.10 and, for even moments, its probability bound.
Concept map
Evidence
This concept declares 2 statements. Each proof establishes one of them relative to its assumptions.
1 moment_bound proven
Lean source view on GitHub
| 1 | import Lax253009.HighDegreeSoundness |
| 2 | import Lax253009.SmallUnionDoubleCovers |
| 3 | import Lax253009.MixedPredicateMoments |
| 4 | |
| 5 | /-! |
| 6 | --- |
| 7 | title: Higher-moment bound for the small-coefficient CNA term |
| 8 | type: theorem |
| 9 | --- |
| 10 | For coefficients of degree at most , squared mass at most one, |
| 11 | and absolute value at most , split the mixed-moment expansion |
| 12 | according to the union size of its double covers. Small unions contribute |
| 13 | the bounds from Lemma 4.16; unions of size at least contribute at |
| 14 | most the total double-cover weight times the mixed-correlation bound. |
| 15 | This gives the normalized higher-moment estimate underlying Lemma 4.10 |
| 16 | and, for even moments, its probability bound. |
| 17 | -/ |
| 18 | |
| 19 | namespace Lax253009.SmallCoefficientSoundness |
| 20 | |
| 21 | open HighDegreeSoundness FiniteProbability |
| 22 | open scoped BigOperators |
| 23 | |
| 24 | noncomputable def boundValue (l m r N : ℕ) (δ q : ℝ) : ℝ := |
| 25 | (∑ t ∈ Finset.range r, (2 : ℝ) ^ m * ((2 : ℝ) ^ t * δ) ^ (m - 2 * t) * |
| 26 | (1 + (3 : ℝ) ^ (l * (4 * t + 1) * 2 ^ (2 * t)))) + |
| 27 | (1 + (3 : ℝ) ^ (l * (2 * m + 1) * 2 ^ m)) * |
| 28 | (q ^ r + (2 : ℝ) ^ m * (2 * (N + 1 : ℝ) * Real.exp (-(N : ℝ) * q ^ 2 / 2))) |
| 29 | |
| 30 | axiom moment_bound {ι κ : Type} [Fintype ι] [DecidableEq ι] |
| 31 | [Fintype κ] [DecidableEq κ] [Nonempty κ] |
| 32 | (n : ℕ) (hn : 0 < n) (hN : Fintype.card κ = 2 * n) |
| 33 | (c : Finset ι → ℝ) (l m r : ℕ) (δ q : ℝ) |
| 34 | (hsmall : ∀ S, |c S| ≤ δ) (hδ : 0 ≤ δ) (hq : 0 ≤ q) (hq1 : q ≤ 1) |
| 35 | (hdegree : ∀ S, l < S.card → c S = 0) (henergy : ∑ S, c S ^ 2 ≤ 1) |
| 36 | (hr : 2 * r ≤ m) : |
| 37 | (𝔼 f : ι → κ, normalizedSum Finset.univ c n f ^ m) ≤ |
| 38 | boundValue l m r (Fintype.card κ) δ q |
| 39 | |
| 40 | axiom tail_bound {ι κ : Type} [Fintype ι] [DecidableEq ι] |
| 41 | [Fintype κ] [DecidableEq κ] [Nonempty κ] |
| 42 | (n : ℕ) (hn : 0 < n) (hN : Fintype.card κ = 2 * n) |
| 43 | (c : Finset ι → ℝ) (l m r : ℕ) (δ q : ℝ) |
| 44 | (hsmall : ∀ S, |c S| ≤ δ) (hδ : 0 ≤ δ) (hq : 0 ≤ q) (hq1 : q ≤ 1) |
| 45 | (hdegree : ∀ S, l < S.card → c S = 0) (henergy : ∑ S, c S ^ 2 ≤ 1) |
| 46 | (hr : 2 * r ≤ m) (hm : Even m) (a : ℝ) (ha : 0 < a) : |
| 47 | probability (fun f : ι → κ ↦ a ≤ normalizedSum Finset.univ c n f) ≤ |
| 48 | boundValue l m r (Fintype.card κ) δ q / a ^ m |
| 49 | |
| 50 | end Lax253009.SmallCoefficientSoundness |
| 51 |
Builds on
Used by
From Mathlib
none
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments