Row averaging for extraction after leakage #
Retaining the row tag makes the joint distance exactly the marginal-weighted
average of row distances. Rows of mass at least K * μ obey the extractor's
conditional cap. Every smaller row is charged its mass, at most K * μ.
theorem
Algebraic.Cutwidth.Extractor.Internal.weightDist_tagged_seededOutput
{Tag : Type u_1}
{Source : Type u_2}
{Seed : Type u_3}
{Out : Type u_4}
[Fintype Tag]
[Fintype Source]
[Fintype Seed]
[Fintype Out]
(E : Source → Seed → Out)
(w : Tag → ℝ)
(p : Tag → Source → ℝ)
(nonnegative : ∀ (t : Tag), 0 ≤ w t)
:
weightDist
(weightedSeededOutput (fun (tx : Tag × Source) => w tx.1 * p tx.1 tx.2) fun (tx : Tag × Source) (y : Seed) =>
(tx.1, E tx.2 y))
(seedFamilyWeight fun (x : Seed) => uniformExtensionWeight Out w) = ∑ t : Tag, w t * weightDist (weightedSeededOutput (p t) E) (seedFamilyWeight fun (x : Seed) => uniformWeight Out)
theorem
Algebraic.Cutwidth.Extractor.Internal.weightedStrongSeededExtractor_leakage_dist_le
{Tag : Type u_1}
{Source : Type u_2}
{Seed : Type u_3}
{Out : Type u_4}
[Fintype Tag]
[Fintype Source]
[Fintype Seed]
[Fintype Out]
[Nonempty Seed]
[Nonempty Out]
{E : Source → Seed → Out}
{K : ℕ}
{ε : ℝ}
(extract : WeightedStrongSeededExtractor E K ε)
(error : 0 ≤ ε)
(p : Tag × Source → ℝ)
(probability : IsProbabilityWeight p)
(μ : Tag → ℝ)
(nonnegative : ∀ (t : Tag), 0 ≤ μ t)
(cap : ∀ (t : Tag) (x : Source), p (t, x) ≤ μ t)
:
weightDist (weightedSeededOutput p fun (tx : Tag × Source) (y : Seed) => (tx.1, E tx.2 y))
(seedFamilyWeight fun (x : Seed) => uniformExtensionWeight Out (firstWeight p)) ≤ ε + ↑K * ∑ t : Tag, μ t
theorem
Algebraic.Cutwidth.Extractor.Internal.weightedStrongSeededExtractor_leakage_average_dist_le
{Tag : Type u_1}
{Source : Type u_2}
{Seed : Type u_3}
{Out : Type u_4}
[Fintype Tag]
[Fintype Source]
[Fintype Seed]
[Fintype Out]
[Nonempty Seed]
[Nonempty Out]
{E : Source → Seed → Out}
{K : ℕ}
{ε : ℝ}
(extract : WeightedStrongSeededExtractor E K ε)
(error : 0 ≤ ε)
(p : Tag × Source → ℝ)
(probability : IsProbabilityWeight p)
(μ : Tag → ℝ)
(nonnegative : ∀ (t : Tag), 0 ≤ μ t)
(cap : ∀ (t : Tag) (x : Source), p (t, x) ≤ μ t)
:
(∑ y : Seed,
weightDist (mapWeight (fun (tx : Tag × Source) => (tx.1, E tx.2 y)) p)
(uniformExtensionWeight Out (firstWeight p))) / ↑(Fintype.card Seed) ≤ ε + ↑K * ∑ t : Tag, μ t