noncomputable def max_val {α : Type u_1} [Fintype α] (a : FinPMF α) : ℝ

Equations

• max_val a = ⨆ (x : α), a x

@[simp]

theorem le_max_val {α : Type u_1} [Fintype α] (a : FinPMF α) {x : α} : a x ≤ max_val a

theorem max_val_le_one {α : Type u_1} [Nonempty α] [Fintype α] (a : FinPMF α) : max_val a ≤ 1

theorem card_inv_le_max_val {α : Type u_1} [Nonempty α] [Fintype α] (a : FinPMF α) : (↑(Fintype.card α))⁻¹ ≤ max_val a

theorem zero_lt_max_val {α : Type u_1} [Nonempty α] [Fintype α] (a : FinPMF α) : 0 < max_val a

noncomputable def min_entropy {α : Type u_1} [Fintype α] (a : FinPMF α) : ℝ

Equations

• min_entropy a = -Real.logb 2 (max_val a)

theorem two_pow_neg_min_entropy_eq_max_val {α : Type u_1} [Nonempty α] [Fintype α] (a : FinPMF α) : 2 ^ (-min_entropy a) = max_val a

theorem min_entropy_of_max_val_le {α : Type u_1} [Nonempty α] [Fintype α] (a : FinPMF α) (k : ℝ) : max_val a ≤ (2 ^ k)⁻¹ ↔ k ≤ min_entropy a

theorem min_entropy_le {α : Type u_1} [Nonempty α] [Fintype α] (a : FinPMF α) (k : ℝ) : min_entropy a ≥ k ↔ ∀ (i : α), a i ≤ 2 ^ (-k)

theorem min_entropy_l2_norm {α : Type u_1} [Nonempty α] [Fintype α] (k : ℕ) (a : FinPMF α) (h : ↑k ≤ min_entropy a) : ‖(WithLp.equiv 2 (α → ℝ)).symm ⇑a‖ ≤ 2 ^ (-↑k / 2)

noncomputable def two_extractor {α : Type u_1} [Fintype α] {β : Type u_2} [Fintype β] {γ : Type u_3} [Nonempty γ] [Fintype γ] (h : α × β → γ) (k : ℝ) (ε : ℝ) : Prop

Equations

• two_extractor h k ε = ∀ (a : FinPMF α) (b : FinPMF β), min_entropy a ≥ k ∧ min_entropy b ≥ k → SD (FinPMF.apply (a * b) h) (Uniform { val := Finset.univ, property := ⋯ }) ≤ ε