theorem card_filter_indexOf_lt {α : Type u_1} [Fintype α] [DecidableEq α] (l : ℕ) (vals : List α) (h : List.Nodup vals) (h₂ : l ≤ List.length vals) : (Finset.filter (fun (x : α) => List.indexOf x vals < l) Finset.univ).card = l

noncomputable def measure_complexity {α : Type u_1} [Fintype α] (a : FinPMF α) (l : ℕ+) : ℕ

Equations

• measure_complexity a l = (Finset.filter (fun (x : α) => a x ≠ 0 ∧ a x ≠ 1 / ↑↑l) Finset.univ).card

theorem split_to_flat_sources {α : Type u_1} [Nonempty α] [Fintype α] [DecidableEq α] (a : FinPMF α) (l : ℕ+) (h : max_val a ≤ 1 / ↑↑l) : ∃ (f : FinPMF { x : Finset α // x.card = ↑l }), (FinPMF.linear_combination f fun (x : { x : Finset α // x.card = ↑l }) => Uniform { val := ↑x, property := ⋯ }) = a