Deficiency.lean`

33 declarations, 0 contain sorry, 0 declared as axioms

Finite distinct-subset-sum estimates

These are the cardinality statements underlying the deficiency lemma in §2 of A Low-Space Algorithm for Worst-Case Subset Sum. The indexed formulation retains repeated input values. Arbitrary signed integer weights are allowed.

def OAI.LowSpaceSubsetSum.distinctSums line 23
Source documentation
Distinct integer values of subset sums on the index domain V.
```
def distinctSums (a : ι → ℤ) (V : Finset ι) : Finset ℤ :=
…
```
def OAI.LowSpaceSubsetSum.distinctSumCount line 27
Source documentation
The count N(V) used in the paper's deficiency.
```
def distinctSumCount (a : ι → ℤ) (V : Finset ι) : ℕ :=
…
```
theorem OAI.LowSpaceSubsetSum.mem_distinctSums line 30
theorem OAI.LowSpaceSubsetSum.zero_mem_distinctSums line 34
theorem OAI.LowSpaceSubsetSum.one_le_distinctSumCount line 38
theorem OAI.LowSpaceSubsetSum.distinctSumCount_le_pow line 42
theorem OAI.LowSpaceSubsetSum.distinctSums_empty line 46
theorem OAI.LowSpaceSubsetSum.distinctSumCount_empty line 49
theorem OAI.LowSpaceSubsetSum.distinctSums_mono line 52
theorem OAI.LowSpaceSubsetSum.distinctSumCount_mono line 56
theorem OAI.LowSpaceSubsetSum.weight_singleton line 60
theorem OAI.LowSpaceSubsetSum.weight_insert_of_not_mem line 63
theorem OAI.LowSpaceSubsetSum.distinctSums_insert_subset line 69
Source documentation
Every sum after adding one index is either an old sum or its translate.
```
theorem distinctSums_insert_subset (a : ι → ℤ) (V : Finset ι) (i : ι) :
    distinctSums a (insert i V) ⊆
      distinctSums a V ∪ (distinctSums a V).image (fun x => a i + x) := by
…
```
Mentions: OAI.LowSpaceSubsetSum.distinctSums
theorem OAI.LowSpaceSubsetSum.distinctSumCount_insert_le line 98
theorem OAI.LowSpaceSubsetSum.distinctSumCount_le_insert line 109
theorem OAI.LowSpaceSubsetSum.distinctSums_union_subset line 115
Source documentation
Every sum on a union is a sum of a value from each domain. The domains need not be disjoint: split a witness using intersection and set difference.
```
theorem distinctSums_union_subset (a : ι → ℤ) (V W : Finset ι) :
    distinctSums a (V ∪ W) ⊆
      ((distinctSums a V) ×ˢ (distinctSums a W)).image (fun p => p.1 + p.2) := by
…
```
Mentions: OAI.LowSpaceSubsetSum.distinctSums
theorem OAI.LowSpaceSubsetSum.distinctSumCount_union_le line 140
Source documentation
The multiplicative count bound behind superadditivity of deficiency.
```
theorem distinctSumCount_union_le (a : ι → ℤ) (V W : Finset ι) :
    distinctSumCount a (V ∪ W) ≤ distinctSumCount a V * distinctSumCount a W := by
…
```
Mentions: OAI.LowSpaceSubsetSum.distinctSumCount
theorem OAI.LowSpaceSubsetSum.symmDiff_subset_domain line 150
theorem OAI.LowSpaceSubsetSum.distinctSums_flip_of_subset line 155
Source documentation
Negating selected indices translates the set of distinct sum values.
```
theorem distinctSums_flip_of_subset (a : ι → ℤ) {F V : Finset ι} (hF : F ⊆ V) :
    distinctSums (flip a F) V = (distinctSums a V).image (fun x => x - weight a F) := by
…
```
Mentions: OAI.LowSpaceSubsetSum.distinctSums, OAI.LowSpaceSubsetSum.flip, OAI.LowSpaceSubsetSum.weight
theorem OAI.LowSpaceSubsetSum.distinctSumCount_flip_of_subset line 172
theorem OAI.LowSpaceSubsetSum.weight_flip_inter line 180
Source documentation
Signs outside the current domain do not affect its subset sums.
```
theorem weight_flip_inter (a : ι → ℤ) (F V : Finset ι) {S : Finset ι} (hS : S ⊆ V) :
    weight (flip a F) S = weight (flip a (F ∩ V)) S := by
…
```
Mentions: OAI.LowSpaceSubsetSum.weight, OAI.LowSpaceSubsetSum.flip
theorem OAI.LowSpaceSubsetSum.distinctSumCount_flip line 190
Source documentation
Distinct-sum counts are invariant under arbitrary individual sign changes.
```
theorem distinctSumCount_flip (a : ι → ℤ) (F V : Finset ι) :
    distinctSumCount (flip a F) V = distinctSumCount a V := by
…
```
Mentions: OAI.LowSpaceSubsetSum.distinctSumCount, OAI.LowSpaceSubsetSum.flip
def OAI.LowSpaceSubsetSum.deficiency line 205
Source documentation
The paper's deficiency, with logarithms in base two.
```
noncomputable def deficiency (a : ι → ℤ) (V : Finset ι) : ℝ :=
…
```
theorem OAI.LowSpaceSubsetSum.distinctSumCount_pos_real line 208
theorem OAI.LowSpaceSubsetSum.deficiency_nonneg line 212
theorem OAI.LowSpaceSubsetSum.deficiency_le_card line 221
theorem OAI.LowSpaceSubsetSum.deficiency_empty line 226
theorem OAI.LowSpaceSubsetSum.deficiency_flip line 231
Source documentation
Sign changes preserve deficiency even when the domain is a proper subset of all indices whose signs are changed.
```
theorem deficiency_flip (a : ι → ℤ) (F V : Finset ι) :
    deficiency (flip a F) V = deficiency a V := by
…
```
Mentions: OAI.LowSpaceSubsetSum.deficiency, OAI.LowSpaceSubsetSum.flip
theorem OAI.LowSpaceSubsetSum.deficiency_superadditive line 236
Source documentation
Deficiency is superadditive on disjoint domains.
```
theorem deficiency_superadditive (a : ι → ℤ) {V W : Finset ι} (hd : Disjoint V W) :
    deficiency a V + deficiency a W ≤ deficiency a (V ∪ W) := by
…
```
Mentions: OAI.LowSpaceSubsetSum.deficiency
theorem OAI.LowSpaceSubsetSum.deficiency_mono line 249
Source documentation
Inclusion monotonicity follows by splitting off the new indices.
```
theorem deficiency_mono (a : ι → ℤ) {V W : Finset ι} (hVW : V ⊆ W) :
    deficiency a V ≤ deficiency a W := by
…
```
Mentions: OAI.LowSpaceSubsetSum.deficiency
theorem OAI.LowSpaceSubsetSum.deficiency_insert_le line 260
Source documentation
Adding a fresh index increases deficiency by at most one.
```
theorem deficiency_insert_le (a : ι → ℤ) {V : Finset ι} {i : ι} (hi : i ∉ V) :
    deficiency a (insert i V) ≤ deficiency a V + 1 := by
…
```
Mentions: OAI.LowSpaceSubsetSum.deficiency
theorem OAI.LowSpaceSubsetSum.deficiency_insert_bounds line 269
theorem OAI.LowSpaceSubsetSum.deficiency_replacement_lipschitz line 276
Source documentation
Replacing one index of a domain by another changes deficiency by at most one, the bounded-difference fact used in the variance estimate.
```
theorem deficiency_replacement_lipschitz (a : ι → ℤ) {V : Finset ι} {i j : ι}
    (hi : i ∉ V) (hj : j ∉ V) :
    |deficiency a (insert i V) - deficiency a (insert j V)| ≤ 1 := by
…
```
Mentions: OAI.LowSpaceSubsetSum.deficiency