Finite sampler amplification proofs #
The neighbors of outer seeds whose every candidate hits a test lie in the base sampler's hit set. Coverage therefore bounds the number of those outer seeds. This pointwise implication transfers the arbitrary weighted failure bound. Seeded extraction gives coverage by testing the full neighbor image.
theorem
Algebraic.Cutwidth.Extractor.Internal.card_allHitSeeds_lt
{α : Type u_1}
{Outer : Type u_2}
{Candidate : Type u_3}
{Base : Type u_4}
{Ω : Type u_5}
[Fintype Outer]
[Fintype Candidate]
[Fintype Base]
[Nonempty Base]
{Γ : Outer → Candidate → Base}
{K : ℕ}
{ρ ε₀ : ℝ}
(cover : NeighborCoverage Γ K ρ)
(separate : 2 * ε₀ < ρ)
(E : α → Base → Ω)
(T : Finset Ω)
(x : α)
(good : ↑(seedHits E T x) ≤ 2 * ε₀ * ↑(Fintype.card Base))
:
theorem
Algebraic.Cutwidth.Extractor.Internal.neighborCoverage_of_flatSeededExtractor
{Outer : Type u_1}
{Candidate : Type u_2}
{Base : Type u_3}
[Fintype Candidate]
[Nonempty Candidate]
[Fintype Base]
{Γ : Outer → Candidate → Base}
{K : ℕ}
{ε : ℝ}
(extract : FlatSeededExtractor Γ K ε)
(positive : 0 < K)
:
NeighborCoverage Γ K (1 - ε)
theorem
Algebraic.Cutwidth.Extractor.Internal.somewhereBadInputs_subset
{α : Type u_1}
{Outer : Type u_2}
{Candidate : Type u_3}
{Base : Type u_4}
{Ω : Type u_5}
[Fintype α]
[Fintype Outer]
[Fintype Candidate]
[Fintype Base]
[Nonempty Base]
{Γ : Outer → Candidate → Base}
{K : ℕ}
{ρ ε₀ ε : ℝ}
(cover : NeighborCoverage Γ K ρ)
(separate : 2 * ε₀ < ρ)
(budget : ↑K ≤ 2 * ε * ↑(Fintype.card Outer))
(E : α → Base → Ω)
(T : Finset Ω)
:
somewhereBadInputs (fun (x : α) (y : Outer) (z : Candidate) => E x (Γ y z)) T ε ⊆ badInputs E T ε₀
theorem
Algebraic.Cutwidth.Extractor.Internal.sampler_amplify
{α : Type u_1}
{Outer : Type u_2}
{Candidate : Type u_3}
{Base : Type u_4}
{Ω : Type u_5}
[Fintype α]
[Fintype Outer]
[Fintype Candidate]
[Fintype Base]
[Fintype Ω]
[Nonempty Base]
{E : α → Base → Ω}
{Γ : Outer → Candidate → Base}
{K : ℕ}
{L ε₀ ε δ ρ : ℝ}
(sample : Sampler E L ε₀ δ)
(cover : NeighborCoverage Γ K ρ)
(small : ε ≤ ε₀)
(separate : 2 * ε₀ < ρ)
(budget : ↑K ≤ 2 * ε * ↑(Fintype.card Outer))
:
SomewhereSampler (fun (x : α) (y : Outer) (z : Candidate) => E x (Γ y z)) L ε δ
theorem
Algebraic.Cutwidth.Extractor.Internal.neighborCoverage_seedProjection
{Outer : Type u_1}
{Base : Type u_2}
[Fintype Base]
{K : ℕ}
(positive : 0 < K)
:
NeighborCoverage (fun (x : Outer) (z : Base) => z) K 1