Finite probability identities for strong seeded extraction #
Product tests forget some or all of the seed information. Counting their source and seed pairs identifies the normalized contract with the existing division-free output-test inequality. Empty sources contribute zero to that inequality and need no probability normalization.
theorem
Algebraic.Cutwidth.Extractor.Internal.uniformSeededTestProb_empty
{Seed : Type u_1}
{Ω : Type u_2}
[Fintype Seed]
[Fintype Ω]
:
theorem
Algebraic.Cutwidth.Extractor.Internal.uniformSeededTestProb_product
{Seed : Type u_1}
{Ω : Type u_2}
[Fintype Seed]
[Fintype Ω]
(S : Finset Seed)
(T : Finset Ω)
:
uniformSeededTestProb (S.product T) = ↑S.card / ↑(Fintype.card Seed) * (↑T.card / ↑(Fintype.card Ω))
theorem
Algebraic.Cutwidth.Extractor.Internal.seededTestProb_univ_product
{α : Type u_1}
{Seed : Type u_2}
{Ω : Type u_3}
[Fintype Seed]
(E : α → Seed → Ω)
(P : Finset α)
(T : Finset Ω)
:
seededTestProb (fun (x : ↥P) => E ↑x) (Finset.univ.product T) = (∑ x ∈ P, ↑(seedHits E T x)) / (↑P.card * ↑(Fintype.card Seed))
theorem
Algebraic.Cutwidth.Extractor.Internal.strong_mono_threshold
{α : Type u_1}
{Seed : Type u_2}
{Ω : Type u_3}
[Fintype Seed]
[Fintype Ω]
{E : α → Seed → Ω}
{K L : ℕ}
{ε : ℝ}
(extract : FlatStrongSeededExtractor E K ε)
(threshold : K ≤ L)
:
theorem
Algebraic.Cutwidth.Extractor.Internal.strong_mono_error
{α : Type u_1}
{Seed : Type u_2}
{Ω : Type u_3}
[Fintype Seed]
[Fintype Ω]
{E : α → Seed → Ω}
{K : ℕ}
{ε δ : ℝ}
(extract : FlatStrongSeededExtractor E K ε)
(error : ε ≤ δ)
:
theorem
Algebraic.Cutwidth.Extractor.Internal.flatSeededExtractor_of_strong
{α : Type u_1}
{Seed : Type u_2}
{Ω : Type u_3}
[Fintype Seed]
[Fintype Ω]
[Nonempty Seed]
[Nonempty Ω]
{E : α → Seed → Ω}
{K : ℕ}
{ε : ℝ}
(extract : FlatStrongSeededExtractor E K ε)
:
FlatSeededExtractor E K ε