Quantitative soundness at a fixed evaluation point
Lax323828.CNAPointSoundness · concepts/Lax323828/CNAPointSoundness.lean · lax-323828
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Theorem
The three Fourier estimates apply to the actual event that every balanced query agrees with evaluation at a fixed point while its label is absent from the small decoding set. This is the fixed-point step in Section 4.1. The table may be real valued and bounded by one, so the same statement applies after averaging over a side condition.
Concept map
Evidence
Lean source view on GitHub
| 1 | import Lax323828.FourierDecoding |
| 2 | import Lax323828.HighDegreeSoundness |
| 3 | import Lax323828.SmallCoefficientSoundness |
| 4 | import Lax323828.LargeCoefficientSoundness |
| 5 | |
| 6 | /-! |
| 7 | --- |
| 8 | title: Quantitative soundness at a fixed evaluation point |
| 9 | type: theorem |
| 10 | --- |
| 11 | The three Fourier estimates apply to the actual event that every balanced |
| 12 | query agrees with evaluation at a fixed point while its label is absent |
| 13 | from the small decoding set. This is the fixed-point step in Section 4.1. |
| 14 | The table may be real valued and bounded by one, so the same statement |
| 15 | applies after averaging over a side condition. |
| 16 | -/ |
| 17 | |
| 18 | namespace Lax323828.CNAPointSoundness |
| 19 | |
| 20 | open BooleanFourier BalancedPredicates FiniteProbability |
| 21 | |
| 22 | noncomputable def decoding {ι : Type} [Fintype ι] [DecidableEq ι] |
| 23 | (F : Cube ι → ℝ) (l : ℕ) (τ : ℝ) : Finset ι := |
| 24 | SmallSupport.decodingSet (coefficient F) l (τ ^ 2 / l) |
| 25 | |
| 26 | def Matches {ι κ : Type} [Fintype κ] [DecidableEq κ] |
| 27 | (F : Cube ι → ℝ) (n : ℕ) (f : ι → κ) (y : ι) : Prop := |
| 28 | ∀ B : predicates κ n, F (fun i ↦ B.val (f i)) = sign (B.val (f y)) |
| 29 | |
| 30 | def Avoids {ι κ : Type} (D : Finset ι) (f : ι → κ) (y : ι) : Prop := |
| 31 | ∀ x ∈ D, f x ≠ f y |
| 32 | |
| 33 | noncomputable def pointBound (l m r N : ℕ) (τ q : ℝ) : ℝ := |
| 34 | 9 * (q ^ l + 2 * (N + 1 : ℝ) * Real.exp (-(N : ℝ) * q ^ 2 / 2)) + |
| 35 | (3 : ℝ) ^ m * SmallCoefficientSoundness.boundValue l m r N τ q |
| 36 | |
| 37 | axiom decoding_card {ι : Type} [Fintype ι] [DecidableEq ι] |
| 38 | (F : Cube ι → ℝ) (hF : ∀ x, |F x| ≤ 1) |
| 39 | (l : ℕ) (hl : 0 < l) (τ : ℝ) (hτ : 0 < τ) : |
| 40 | ((decoding F l τ).card : ℝ) ≤ (l : ℝ) / τ ^ 2 |
| 41 | |
| 42 | axiom point_soundness {ι κ : Type} [Fintype ι] [DecidableEq ι] |
| 43 | [Fintype κ] [DecidableEq κ] [Nonempty κ] |
| 44 | (F : Cube ι → ℝ) (hF : ∀ x, |F x| ≤ 1) |
| 45 | (n : ℕ) (hn : 0 < n) (hN : Fintype.card κ = 2 * n) |
| 46 | (l m r : ℕ) (hl : 0 < l) (hlN : l < Fintype.card κ) |
| 47 | (τ q : ℝ) (hτ : 0 < τ) (hq : 0 ≤ q) (hq1 : q ≤ 1) |
| 48 | (hr : 2 * r ≤ m) (hm : Even m) |
| 49 | (hlarge : (l : ℝ) / ((Fintype.card κ : ℝ) - l) / τ ≤ 1 / 3) |
| 50 | (y : ι) : |
| 51 | probability (fun f : ι → κ ↦ Matches F n f y ∧ Avoids (decoding F l τ) f y) ≤ |
| 52 | pointBound l m r (Fintype.card κ) τ q |
| 53 | |
| 54 | end Lax323828.CNAPointSoundness |
| 55 |
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments