def FinPMF (α : Type u_8) [Fintype α] : Type u_8

Equations

• FinPMF α = { f : α → ℝ // (Finset.sum Finset.univ fun (x : α) => f x) = 1 ∧ ∀ (x : α), f x ≥ 0 }

instance instFunLike {α : Type u_1} [Fintype α] : FunLike (FinPMF α) α ℝ

Equations

• instFunLike = { coe := fun (p : FinPMF α) => ↑p, coe_injective' := ⋯ }

@[simp]

theorem FinPMF.sum_coe {α : Type u_1} [Fintype α] (p : FinPMF α) : (Finset.sum Finset.univ fun (a : α) => p a) = 1

theorem FinPMF.val_apply {α : Type u_1} [Fintype α] {x : α} (f : FinPMF α) : f x = ↑f x

theorem FinPMF.val_mk {α : Type u_1} [Fintype α] (f : α → ℝ) {h : (Finset.sum Finset.univ fun (x : α) => f x) = 1 ∧ ∀ (x : α), f x ≥ 0} : ↑{ val := f, property := h } = f

@[simp]

theorem FinPMF.nonneg {α : Type u_1} [Fintype α] {x : α} (p : FinPMF α) : 0 ≤ p x

noncomputable def Uniform {α : Type u_1} [Fintype α] [DecidableEq α] (t : { x : Finset α // x.Nonempty }) : FinPMF α

Equations

• Uniform t = { val := fun (x : α) => if x ∈ ↑t then 1 / ↑(↑t).card else 0, property := ⋯ }

noncomputable def Uniform_singleton {α : Type u_1} [Fintype α] [DecidableEq α] (x : α) : FinPMF α

Equations

• Uniform_singleton x = Uniform { val := {x}, property := ⋯ }

@[simp]

theorem uniform_single_value {α : Type u_1} [Fintype α] [DecidableEq α] (x : α) (y : α) : (Uniform_singleton x) y = if y = x then 1 else 0

@[simp]

theorem Uniform.univ_uniform {α : Type u_1} [Fintype α] [DecidableEq α] {x : α} [Nonempty α] : (Uniform { val := Finset.univ, property := ⋯ }) x = 1 / ↑(Fintype.card α)

instance instMulFinPMF {α : Type u_1} [Fintype α] {β : Type u_2} [Fintype β] : HMul (FinPMF α) (FinPMF β) (FinPMF (α × β))

Equations

• instMulFinPMF = { hMul := fun (a : FinPMF α) (b : FinPMF β) => { val := fun (x : α × β) => a x.1 * b x.2, property := ⋯ } }

@[simp]

theorem FinPMF.mul_val {α : Type u_1} [Fintype α] {β : Type u_2} [Fintype β] {x : α} {y : β} (a : FinPMF α) (b : FinPMF β) : (a * b) (x, y) = a x * b y

noncomputable def FinPMF.apply {α : Type u_1} [Fintype α] [DecidableEq α] {β : Type u_2} [Fintype β] [DecidableEq β] (a : FinPMF α) (f : α → β) : FinPMF β

Equations

• FinPMF.apply a f = { val := f # ⇑a, property := ⋯ }

theorem apply_weighted_sum {α : Type u_1} [Fintype α] [DecidableEq α] {β : Type u_2} [Fintype β] [DecidableEq β] {𝕜 : Type u_3} [RCLike 𝕜] (a : FinPMF α) (g : α → β) (f : β → 𝕜) : (Finset.sum Finset.univ fun (x : β) => ↑((FinPMF.apply a g) x) * f x) = Finset.sum Finset.univ fun (y : α) => ↑(a y) * f (g y)

theorem FinPMF.apply_equiv {α : Type u_1} [Fintype α] [DecidableEq α] {β : Type u_2} [Fintype β] [DecidableEq β] {y : β} (a : FinPMF α) (f : α ≃ β) : (FinPMF.apply a ⇑f) y = a (f.symm y)

theorem FinPMF.apply_swap {α : Type u_1} [Fintype α] [DecidableEq α] {β : Type u_2} [Fintype β] [DecidableEq β] (a : FinPMF α) (b : FinPMF β) : FinPMF.apply (a * b) Prod.swap = b * a

theorem FinPMF.apply_apply {α : Type u_1} [Fintype α] [DecidableEq α] {β : Type u_2} [Fintype β] [DecidableEq β] {γ : Type u_4} (a : FinPMF α) (f : α → β) (g : β → γ) [Nonempty γ] [Fintype γ] [DecidableEq γ] : FinPMF.apply (FinPMF.apply a f) g = FinPMF.apply a (g ∘ f)

theorem FinPMF.eq_apply_id {α : Type u_1} [Fintype α] [DecidableEq α] (a : FinPMF α) : FinPMF.apply a id = a

noncomputable instance instSubFinPMF {α : Type u_1} [Fintype α] [DecidableEq α] [Sub α] : Sub (FinPMF α)

Equations

• instSubFinPMF = { sub := fun (a b : FinPMF α) => FinPMF.apply (a * b) fun (x : α × α) => x.1 - x.2 }

noncomputable instance instAddFinPMF {α : Type u_1} [Fintype α] [DecidableEq α] [Add α] : Add (FinPMF α)

Equations

• instAddFinPMF = { add := fun (a b : FinPMF α) => FinPMF.apply (a * b) fun (x : α × α) => x.1 + x.2 }

noncomputable instance instNegFinPMF {α : Type u_1} [Fintype α] [DecidableEq α] [Neg α] : Neg (FinPMF α)

Equations

• instNegFinPMF = { neg := fun (a : FinPMF α) => FinPMF.apply a fun (x : α) => -x }

noncomputable instance instZeroFinPMF {α : Type u_1} [Fintype α] [DecidableEq α] [Zero α] : Zero (FinPMF α)

Equations

• instZeroFinPMF = { zero := { val := fun (x : α) => if x = 0 then 1 else 0, property := ⋯ } }

@[simp]

theorem FinPMF.neg_apply {α : Type u_1} [Fintype α] [DecidableEq α] {x : α} (a : FinPMF α) [InvolutiveNeg α] : (-a) x = a (-x)

@[simp]

theorem FinPMF.neg_neg {α : Type u_1} [Fintype α] [DecidableEq α] (a : FinPMF α) [InvolutiveNeg α] : - -a = a

theorem FinPMF.neg_add {α : Type u_1} [Fintype α] [DecidableEq α] (a : FinPMF α) (b : FinPMF α) [AddCommGroup α] : -(a + b) = -a + -b

theorem FinPMF.sub_eq_add_neg {α : Type u_1} [Fintype α] [DecidableEq α] (a : FinPMF α) (b : FinPMF α) [AddGroup α] : a - b = a + -b

noncomputable instance FinPMFCommMonoid {α : Type u_1} [Fintype α] [DecidableEq α] [AddCommGroup α] : AddCommMonoid (FinPMF α)

Equations

• FinPMFCommMonoid = AddCommMonoid.mk ⋯

theorem FinPMF.sub_val {α : Type u_1} [Fintype α] [DecidableEq α] (a : FinPMF α) (b : FinPMF α) [Sub α] : a - b = FinPMF.apply (a * b) fun (x : α × α) => x.1 - x.2

theorem FinPMF.add_val {α : Type u_1} [Fintype α] [DecidableEq α] (a : FinPMF α) (b : FinPMF α) [Add α] : a + b = FinPMF.apply (a * b) fun (x : α × α) => x.1 + x.2

theorem FinPMF.apply_mul {α : Type u_1} [Fintype α] [DecidableEq α] {β : Type u_2} [Fintype β] [DecidableEq β] {γ : Type u_4} {γ₂ : Type u_5} (a : FinPMF α) (b : FinPMF β) (f : α → γ) (g : β → γ₂) [Nonempty γ] [Fintype γ] [DecidableEq γ] [Nonempty γ₂] [Fintype γ₂] [DecidableEq γ₂] : FinPMF.apply a f * FinPMF.apply b g = FinPMF.apply (a * b) fun (x : α × β) => (f x.1, g x.2)

theorem FinPMF.apply_add {α : Type u_1} [Fintype α] [DecidableEq α] {β : Type u_2} [Fintype β] [DecidableEq β] {γ : Type u_4} (a : FinPMF α) (b : FinPMF β) (f : α → γ) (g : β → γ) [Nonempty γ] [Fintype γ] [Add γ] [DecidableEq γ] : FinPMF.apply a f + FinPMF.apply b g = FinPMF.apply (a * b) fun (x : α × β) => f x.1 + g x.2

theorem apply_ne_zero {α : Type u_1} [Fintype α] [DecidableEq α] {β : Type u_2} [Fintype β] [DecidableEq β] (a : FinPMF α) (f : α → β) (x : β) (h : (FinPMF.apply a f) x ≠ 0) : ∃ (i : α), x = f i

noncomputable def FinPMF.linear_combination {α : Type u_1} [Fintype α] {β : Type u_2} [Fintype β] (a : FinPMF α) (f : α → FinPMF β) : FinPMF β

Equations

• FinPMF.linear_combination a f = { val := fun (x : β) => Finset.sum Finset.univ fun (y : α) => a y * (f y) x, property := ⋯ }

theorem linear_combination_linear_combination {α : Type u_1} [Fintype α] {β : Type u_2} [Fintype β] {γ : Type u_4} [Fintype γ] (a : FinPMF α) (f : α → FinPMF β) (g : β → FinPMF γ) : FinPMF.linear_combination (FinPMF.linear_combination a f) g = FinPMF.linear_combination a fun (x : α) => FinPMF.linear_combination (f x) g

theorem linear_combination_apply {α : Type u_1} [Fintype α] {β : Type u_2} [Fintype β] [DecidableEq β] {γ : Type u_4} [Nonempty γ] [Fintype γ] [DecidableEq γ] (a : FinPMF α) (f : α → FinPMF β) (g : β → γ) : FinPMF.apply (FinPMF.linear_combination a f) g = FinPMF.linear_combination a fun (x : α) => FinPMF.apply (f x) g

theorem linear_combination_mul {α : Type u_1} [Fintype α] {β : Type u_2} [Fintype β] {α' : Type u_6} {β' : Type u_7} [Nonempty α'] [Fintype α'] [Nonempty β'] [Fintype β'] (a : FinPMF α) (f : α → FinPMF α') (b : FinPMF β) (g : β → FinPMF β') : FinPMF.linear_combination a f * FinPMF.linear_combination b g = FinPMF.linear_combination (a * b) fun (x : α × β) => match x with | (x, y) => f x * g y

noncomputable def FinPMF.adjust {α : Type u_1} [Fintype α] [DecidableEq α] (a : FinPMF α) (x : α) (p : ℝ) (h₁ : 0 ≤ p) (h₂ : p ≤ 1) : FinPMF α

Equations

• FinPMF.adjust a x p h₁ h₂ = FinPMF.linear_combination { val := ![1 - p, p], property := ⋯ } ![a, Uniform_singleton x]

noncomputable def close_high_entropy {α : Type u_1} [Fintype α] (n : ℝ) (ε : ℝ) (a : FinPMF α) : Prop

Equations

• close_high_entropy n ε a = ∀ (H : Finset α), ↑H.card ≤ n → (Finset.sum H fun (v : α) => a v) ≤ ε

theorem close_high_entropy_of_floor {α : Type u_1} [Fintype α] (n : ℝ) (ε : ℝ) (a : FinPMF α) (h : close_high_entropy (↑⌊n⌋₊) ε a) : close_high_entropy n ε a

theorem close_high_entropy_of_le {α : Type u_1} [Fintype α] (n : ℝ) (ε₁ : ℝ) (ε₂ : ℝ) (hε : ε₁ ≤ ε₂) (a : FinPMF α) (h : close_high_entropy n ε₁ a) : close_high_entropy n ε₂ a

theorem close_high_entropy_apply_equiv {α : Type u_1} [DecidableEq α] {β : Type u_2} [DecidableEq β] [Fintype α] [Nonempty α] [Fintype β] [Nonempty β] (n : ℝ) (ε : ℝ) (a : FinPMF α) (h : close_high_entropy n ε a) (e : α ≃ β) : close_high_entropy n ε (FinPMF.apply a ⇑e)

theorem add_close_high_entropy {α : Type u_1} [DecidableEq α] [Fintype α] [Nonempty α] [AddCommGroup α] (n : ℝ) (ε : ℝ) (a : FinPMF α) (b : FinPMF α) (h : close_high_entropy n ε a) : close_high_entropy n ε (a + b)

theorem close_high_entropy_linear_combination {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] [DecidableEq β] (n : ℝ) (ε : ℝ) (a : FinPMF β) (g : β → FinPMF α) (h : ∀ (x : β), 0 < a x → close_high_entropy n ε (g x)) : close_high_entropy n ε (FinPMF.linear_combination a g)

theorem filter_neg_le_inv_card_le {α : Type u_1} [Fintype α] (a : FinPMF α) (n : ℝ) (hn : 0 < n) : ↑(Finset.filter (fun (x : α) => ¬a x ≤ 1 / n) Finset.univ).card ≤ n