Impact function

noncomputable def Finset.mulImpact {α : Type u_1} [DecidableEq α] [Mul α] (s : Finset α) (n : ℕ) : ℕ

The multiplicative impact function of a finset.

Equations

• s.mulImpact n = ⨅ (t : { t : Finset α // t.card = n }), (s * ↑t).card

noncomputable def Finset.addImpact {α : Type u_1} [DecidableEq α] [Add α] (s : Finset α) (n : ℕ) : ℕ

Equations

• s.addImpact n = ⨅ (t : { t : Finset α // t.card = n }), (s + ↑t).card

@[simp]

theorem Finset.mulImpact_empty {α : Type u_1} [DecidableEq α] [Mul α] (n : ℕ) : ∅.mulImpact n = 0

@[simp]

theorem Finset.addImpact_empty {α : Type u_1} [DecidableEq α] [Add α] (n : ℕ) : ∅.addImpact n = 0

@[simp]

theorem Finset.mulImpact_singleton {α : Type u_1} [DecidableEq α] [Group α] [Infinite α] (a : α) (n : ℕ) : {a}.mulImpact n = n

@[simp]

theorem Finset.addImpact_singleton {α : Type u_1} [DecidableEq α] [AddGroup α] [Infinite α] (a : α) (n : ℕ) : {a}.addImpact n = n

theorem Finset.exists_mulImpact_add_mulImpact {α : Type u_1} [DecidableEq α] [Group α] {n : ℕ} [Fintype α] (s : Finset α) (hn : 2 ≤ n) (hnα : n < Fintype.card α) (hnα' : ¬n ∣ Fintype.card α) : ∃ (k : ℕ), 0 < k ∧ k < n ∧ s.mulImpact (n - k) + s.mulImpact (n + k) ≤ 2 * s.mulImpact n

theorem Finset.exists_addImpact_add_addImpact {α : Type u_1} [DecidableEq α] [AddGroup α] {n : ℕ} [Fintype α] (s : Finset α) (hn : 2 ≤ n) (hnα : n < Fintype.card α) (hnα' : ¬n ∣ Fintype.card α) : ∃ (k : ℕ), 0 < k ∧ k < n ∧ s.addImpact (n - k) + s.addImpact (n + k) ≤ 2 * s.addImpact n

theorem Finset.mulImpact_map_of_infinite {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] [CommGroup α] [CommGroup β] {n : ℕ} [Infinite α] (s : Finset α) (f : α →* β) (hf : Function.Injective ⇑f) : (map { toFun := ⇑f, inj' := hf } s).mulImpact n = s.mulImpact n

theorem Finset.addImpact_map_of_infinite {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] [AddCommGroup α] [AddCommGroup β] {n : ℕ} [Infinite α] (s : Finset α) (f : α →+ β) (hf : Function.Injective ⇑f) : (map { toFun := ⇑f, inj' := hf } s).addImpact n = s.addImpact n

theorem Finset.mulImpact_map_of_fintype {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] [CommGroup α] [CommGroup β] {n : ℕ} [Fintype α] (s : Finset α) (f : α →* β) (hf : Function.Injective ⇑f) : (map { toFun := ⇑f, inj' := hf } s).mulImpact n = s.mulImpact (Fintype.card α * (n / Fintype.card α))

theorem Finset.addImpact_map_of_fintype {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] [AddCommGroup α] [AddCommGroup β] {n : ℕ} [Fintype α] (s : Finset α) (f : α →+ β) (hf : Function.Injective ⇑f) : (map { toFun := ⇑f, inj' := hf } s).addImpact n = s.addImpact (Fintype.card α * (n / Fintype.card α))