Reindexing outer seeds and candidate lists #
Bijections of either sampler index preserve every all-candidate hitting event. The bad-input sets and the source-weighted failure bound therefore remain unchanged.
theorem
Algebraic.Cutwidth.Extractor.Internal.allHitSeeds_reindex_card
{α : Type u_1}
{Outer : Type u_2}
{Outer' : Type u_3}
{Candidate : Type u_4}
{Candidate' : Type u_5}
{Ω : Type u_6}
[Fintype Outer]
[Fintype Outer']
(S : α → Outer → Candidate → Ω)
(outer : Outer' ≃ Outer)
(candidate : Candidate' ≃ Candidate)
(T : Finset Ω)
(x : α)
:
(allHitSeeds (fun (x : α) (y : Outer') (z : Candidate') => S x (outer y) (candidate z)) T x).card = (allHitSeeds S T x).card
theorem
Algebraic.Cutwidth.Extractor.Internal.somewhereSampler_reindex
{α : Type u_1}
{Outer : Type u_2}
{Outer' : Type u_3}
{Candidate : Type u_4}
{Candidate' : Type u_5}
{Ω : Type u_6}
[Fintype α]
[Fintype Outer]
[Fintype Outer']
[Fintype Ω]
{S : α → Outer → Candidate → Ω}
{L ε δ : ℝ}
(sample : SomewhereSampler S L ε δ)
(outer : Outer' ≃ Outer)
(candidate : Candidate' ≃ Candidate)
:
SomewhereSampler (fun (x : α) (y : Outer') (z : Candidate') => S x (outer y) (candidate z)) L ε δ