Good source fixings supplied by a somewhere sampler #
Apply the sampler to the uniform weights on the second-source support.
The complement of its bad inputs retains at least a 1 - δ fraction of
the support, and on each retained input at most a 2ε fraction of outer
coordinates has all candidate seeds in the test set.
theorem
Algebraic.Cutwidth.Extractor.Internal.somewhereSampler_exists_good_fibers
{α : Type u_1}
{Outer : Type u_2}
{Candidate : Type u_3}
{Ω : Type u_4}
[Fintype α]
[Fintype Outer]
[Fintype Ω]
{S : α → Outer → Candidate → Ω}
{L ε δ : ℝ}
(sampler : SomewhereSampler S L ε δ)
(Q : Finset α)
(positive : 0 < Q.card)
(source : L ≤ ↑Q.card)
(T : Finset Ω)
(small : ↑T.card ≤ ε * ↑(Fintype.card Ω))
:
theorem
Algebraic.Cutwidth.Extractor.Internal.parityBiasBound_of_seed_escape
{α : Type u_1}
{Choice : Type u_2}
{Seed : Type u_3}
[Fintype Choice]
{m N : ℕ}
{s : Finset α}
{w : α → ℝ}
{σ : α → Fin N → ℝ}
{β : ℝ}
(S : Fin N → Choice → Seed)
(bad : Finset (Fin N) → Choice → Finset Seed)
(good : Fin m ↪ Fin N)
(escape : ∀ (i : Fin m), ∃ (z : Choice), S (good i) z ∉ parityBadSeeds bad 4)
(estimate :
∀ U ∈ parityTests (Fin N) 4,
∃ j ∈ U, ∀ (z : Choice), S j z ∉ bad U z → |weightedMean s w fun (x : α) => ∏ i ∈ U, σ x i| ≤ β)
:
ParityBiasBound s w (fun (x : α) (i : Fin m) => σ x (good i)) β
theorem
Algebraic.Cutwidth.Extractor.Internal.somewhereSampler_parity_fibers
{α : Type u_1}
{Source : Type u_2}
{Choice : Type u_3}
{Seed : Type u_4}
[Fintype Source]
[Fintype Choice]
[Fintype Seed]
{N : ℕ}
{s : Finset α}
{w : α → ℝ}
(σ : α → Source → Fin N → ℝ)
{S : Source → Fin N → Choice → Seed}
{L ε δ β η : ℝ}
(sampler : SomewhereSampler S L ε δ)
(Q : Finset Source)
(positive : 0 < Q.card)
(source : L ≤ ↑Q.card)
(bad : Finset (Fin N) → Choice → Finset Seed)
(nonneg : 0 ≤ η)
(seedBound : ∀ U ∈ parityTests (Fin N) 4, ∀ (z : Choice), ↑(bad U z).card ≤ η * ↑(Fintype.card Seed))
(budget : ↑N ^ 4 * ↑(Fintype.card Choice) * η ≤ ε)
(estimate :
∀ U ∈ parityTests (Fin N) 4,
∃ j ∈ U, ∀ (z : Choice), ∀ y ∈ Q, S y j z ∉ bad U z → |weightedMean s w fun (x : α) => ∏ i ∈ U, σ x y i| ≤ β)
: