Quantitative soundness at a fixed evaluation point
Lax253009.CNAPointSoundness · concepts/Lax253009/CNAPointSoundness.lean · lax-253009
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 Lax253009.FourierDecoding |
| 2 | import Lax253009.HighDegreeSoundness |
| 3 | import Lax253009.SmallCoefficientSoundness |
| 4 | import Lax253009.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 Lax253009.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 Lax253009.CNAPointSoundness |
| 55 |
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments