Maximum n-times coverage

DefinitionCover count of an element under a family of overlays#✓fully proved

The number of times the overlays O cover the element i (equation (1)).

def coverCount (c : A → X → ℕ) (O : Finset A) (i : X) : ℕ := ∑ j ∈ O, c j i

Used by 5

Used byMonotonicity of the cover count in the overlays · Weighted maximum coverage is submodular · The n-times coverage function · Monotonicity of n-times coverage for nonnegative weights · The n-times coverage function is not submodular

DefinitionThe n-times coverage function#✓fully proved

The n-times coverage function: the total weight of the elements covered at least n times by O (equation (2)).

def nCoverage [Fintype X] (w : X → ℝ) (c : A → X → ℕ) (n : ℕ) (O : Finset A) : ℝ :=
  ∑ i, if n ≤ coverCount c O i then w i else 0

Uses 1 · Used by 3

Statement usesCover count of an element under a family of overlays

Used byWeighted maximum coverage is submodular · Monotonicity of n-times coverage for nonnegative weights · The n-times coverage function is not submodular

DefinitionSubmodular set function#✓fully proved

A set function is submodular if adding an element to a larger set gains at most as much as adding it to a smaller set (the diminishing-returns form, Definition 2 of the paper).

def IsSubmodular [DecidableEq A] (f : Finset A → ℝ) : Prop :=
  ∀ S T : Finset A, ∀ x, S ⊆ T → x ∉ T → f (insert x T) - f T ≤ f (insert x S) - f S

Used by 2

Used byWeighted maximum coverage is submodular · The n-times coverage function is not submodular

TheoremMonotonicity of the cover count in the overlays#✓fully proved

More overlays cover every element at least as often.

theorem coverCount_mono (c : A → X → ℕ) {O O' : Finset A} (h : O ⊆ O') (i : X) :
    coverCount c O i ≤ coverCount c O' i

Uses 1 · Used by 2

Statement usesCover count of an element under a family of overlays

Used byWeighted maximum coverage is submodular · Monotonicity of n-times coverage for nonnegative weights

TheoremMonotonicity of n-times coverage for nonnegative weights#✓fully proved

For nonnegative weights the n-times coverage function is monotone.

theorem nCoverage_mono [Fintype X] {w : X → ℝ} (hw : ∀ i, 0 ≤ w i) (c : A → X → ℕ) (n : ℕ)
    {O O' : Finset A} (h : O ⊆ O') : nCoverage w c n O ≤ nCoverage w c n O'

Uses 3

Statement usesThe n-times coverage function

Proof usesCover count of an element under a family of overlays · Monotonicity of the cover count in the overlays

TheoremThe n-times coverage function is not submodular#✓fully proved

The n-times coverage function is not submodular (Liu et al., Theorem 1): for every n ≥ 2, take n overlays that each cover a single element of weight 1 once. Adding the last overlay to the other n - 1 gains 1; adding it to ∅ gains 0.

theorem not_isSubmodular_nCoverage {n : ℕ} (hn : 2 ≤ n) :
    ¬IsSubmodular (nCoverage (fun _ : Unit => (1 : ℝ)) (fun (_ : Fin n) _ => 1) n)

Uses 3

Statement usesSubmodular set function · The n-times coverage function

Proof usesCover count of an element under a family of overlays

TheoremWeighted maximum coverage is submodular#✓fully proved

For n = 1 (weighted maximum coverage) and nonnegative weights, the objective is submodular.

theorem isSubmodular_nCoverage_one [Fintype X] [DecidableEq A] {w : X → ℝ}
    (hw : ∀ i, 0 ≤ w i) (c : A → X → ℕ) : IsSubmodular (nCoverage w c 1)

Uses 4

Statement usesSubmodular set function · The n-times coverage function

Proof usesCover count of an element under a family of overlays · Monotonicity of the cover count in the overlays

7 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.