Conditional information in independent samples

Conditional information content averages to conditional Shannon entropy. If every positive joint mass is at least 2 ^ (-bound), then each sample's conditional information lies between zero and bound. Hoeffding's inequality therefore controls the lower tail of its sum.

Main results

• Cslib.Probability.PMF.uniform_map_mass_ge: a supported image has at least one seed's mass.
• Cslib.Probability.PMF.surprisal_pi: information adds across independent coordinates.
• Cslib.Probability.PMF.pi_sum_conditionalSurprisal_le: concentration of conditional information.
• Cslib.Probability.PMF.pi_conditional_mass_gt: the corresponding conditional-mass tail bound.

References

• T. Holenstein, Pseudorandom Generators from One-Way Functions: A Simple Construction for Any Hardness, Section 3.3, Proposition 1 and Lemma 2. We use a bounded-information variant for deterministic images of uniform finite seeds. Its loss depends on the seed length rather than Proposition 1's sharper alphabet-size bound. Smoothing and leftover hashing are separate steps.

Adapted from Probability/EntropyConcentration.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8.

theorem Cslib.Probability.PMF.uniform_map_mass_ge {Seed : Type u_1} {Output : Type u_2} [Fintype Seed] [Nonempty Seed] (f : Seed → Output) (output : Output) (houtput : output ∈ (PMF.map f (uniformOfFintype Seed)).support) : 2 ^ (-Real.logb 2 ↑(Fintype.card Seed)) ≤ ((PMF.map f (uniformOfFintype Seed)) output).toReal

Every observable image of a uniform finite seed has probability at least one over the seed space size, equivalently 2 ^ (-log₂(card Seed)).

theorem Cslib.Probability.PMF.surprisal_pi {ι : Type u_1} [Fintype ι] {α : ι → Type u_2} [∀ (i : ι), Finite (α i)] (p : (i : ι) → PMF (α i)) (outcome : (i : ι) → α i) (houtcome : outcome ∈ (pi p).support) : surprisal (pi p) outcome = ∑ i : ι, surprisal (p i) (outcome i)

Information content adds across independent coordinates on the product's support.

theorem Cslib.Probability.PMF.pi_sum_conditionalSurprisal_le {ι : Type u_1} [Fintype ι] {α : ι → Type u_2} {β : ι → Type u_3} [∀ (i : ι), Finite (α i)] [∀ (i : ι), Finite (β i)] (joint : (i : ι) → PMF (α i × β i)) {bound ε : ℝ} (hbound : 0 ≤ bound) (hmass : ∀ (i : ι), ∀ pair ∈ (joint i).support, 2 ^ (-bound) ≤ ((joint i) pair).toReal) (hε : 0 ≤ ε) : ((pi joint).toOuterMeasure {outcome : (i : ι) → α i × β i | ∑ i : ι, surprisal (conditionalSnd (joint i) (outcome i).1) (outcome i).2 ≤ ∑ i : ι, conditionalEntropy (joint i) - ε}).toReal ≤ Real.exp (-2 * ε ^ 2 / (↑(Fintype.card ι) * bound ^ 2))

Independent conditional information concentrates around the sum of conditional entropies. Only outcomes in the support need a probability lower bound.

theorem Cslib.Probability.PMF.pi_conditional_mass_gt {ι : Type u_1} [Fintype ι] {α : ι → Type u_2} {β : ι → Type u_3} [∀ (i : ι), Finite (α i)] [∀ (i : ι), Finite (β i)] (joint : (i : ι) → PMF (α i × β i)) {bound ε : ℝ} (hbound : 0 ≤ bound) (hmass : ∀ (i : ι), ∀ pair ∈ (joint i).support, 2 ^ (-bound) ≤ ((joint i) pair).toReal) (hε : 0 ≤ ε) : have repeated := PMF.map (fun (outcome : (i : ι) → α i × β i) => (fun (i : ι) => (outcome i).1, fun (i : ι) => (outcome i).2)) (pi joint); (repeated.toOuterMeasure {pair : ((i : ι) → α i) × ((i : ι) → β i) | 2 ^ (-(∑ i : ι, conditionalEntropy (joint i) - ε)) < ((conditionalSnd repeated pair.1) pair.2).toReal}).toReal ≤ Real.exp (-2 * ε ^ 2 / (↑(Fintype.card ι) * bound ^ 2))

Except with exponentially small probability, the conditional mass of an independent tuple is at most 2 ^ (-(sum of conditional entropies - ε)). All observations are revealed together; null observation tuples do not affect the bound.