/-
Copyright 2025 The Formal Conjectures Authors.
Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at
https://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/
module
public import Mathlib.Algebra.BigOperators.Group.Finset.Basic
public import Mathlib.Algebra.Order.BigOperators.Group.Finset
public import Mathlib.Data.Set.Finite.Lattice
public import Mathlib.Order.Filter.AtTopBot.Basic
public import Mathlib.Order.Filter.AtTopBot.Defs
public import Mathlib.Order.Interval.Finset.Nat
public import Mathlib.Order.WellFounded@[expose] public sectionvariable {M : Type*} [AddCommMonoid M]open scoped List
The set of subset sums of a set A ⊆ M.
def subsetSums (A : Set M) : Set M :=
{n | ∃ B : Finset M, ↑B ⊆ A ∧ n = ∑ i ∈ B, i}
If A ⊆ B, then subsetSums A ⊆ subsetSums B.
@[gcongr]
theorem subsetSums_mono {A B : Set M} (h : A ⊆ B) : subsetSums A ⊆ subsetSums B :=
fun _ ⟨C, hC⟩ => ⟨C, hC.1.trans h, hC.2⟩
The set of subset sums of a sequence ℕ → M, where repetition is allowed.
def subseqSums' (A : ℕ → M) : Set M :=
{n | ∃ B : Finset ℕ, n = ∑ i ∈ B, A i}variable [Preorder M]
A set A ⊆ M is complete if every sufficiently large element of M is a subset sum of A.
def IsAddComplete (A : Set M) : Prop :=
∀ᶠ k in Filter.atTop, k ∈ subsetSums A
If A ⊆ B and A is complete, then B is also complete.
@[gcongr]
theorem IsAddComplete.mono {A B : Set M} (h : A ⊆ B) (ha : IsAddComplete A) : IsAddComplete B := M:Type u_1inst✝¹:AddCommMonoid Minst✝:Preorder MA:Set MB:Set Mh:A ⊆ Bha:IsAddComplete A⊢ IsAddComplete B
filter_upwards [ha] with x M:Type u_1inst✝¹:AddCommMonoid Minst✝:Preorder MA:Set MB:Set Mh:A ⊆ Bha:IsAddComplete Ax:Mhx:x ∈ subsetSums A⊢ x ∈ subsetSums B
All goals completed! 🐙
A set A ⊆ M is complete if every sufficiently large element of M is a subset sum of A.
def IsAddStronglyComplete (A : Set M) : Prop :=
∀ ⦃B : Set M⦄, B.Finite → IsAddComplete (A \ B)A strongly complete set is complete.
theorem IsAddStronglyComplete.isAddComplete {A : Set M} (hA : IsAddStronglyComplete A) :
IsAddComplete A := M:Type u_1inst✝¹:AddCommMonoid Minst✝:Preorder MA:Set MhA:IsAddStronglyComplete A⊢ IsAddComplete A All goals completed! 🐙
If A ⊆ B and A is strongly complete, then B is also strongly complete.
theorem IsAddStronglyComplete.mono {A B : Set M} (h : A ⊆ B) (ha : IsAddStronglyComplete A) :
IsAddStronglyComplete B := fun C hC => (ha hC).mono (M:Type u_1inst✝¹:AddCommMonoid Minst✝:Preorder MA:Set MB:Set Mh:A ⊆ Bha:IsAddStronglyComplete AC:Set MhC:C.Finite⊢ A \ C ⊆ B \ C All goals completed! 🐙)
A sequence A is strongly complete if fun m => A (n + m) is still complete for all n.
def IsAddStronglyCompleteNatSeq (A : ℕ → M) : Prop :=
∀ n, IsAddComplete (Set.range (fun m => A (n + m)))A strongly complete sequence is complete.
theorem IsAddStronglyCompleteNatSeq.isAddComplete {A : ℕ → M}
(hA : IsAddStronglyCompleteNatSeq A) :
IsAddComplete (Set.range A) := M:Type u_1inst✝¹:AddCommMonoid Minst✝:Preorder MA:ℕ → MhA:IsAddStronglyCompleteNatSeq A⊢ IsAddComplete (Set.range A) All goals completed! 🐙open scoped Classical in
If the range of a sequence A is strongly complete, then A is strongly complete.
theorem IsAddStronglyCompleteNatSeq.of_isAddStronglyComplete {A : ℕ → M}
(h : IsAddStronglyComplete (.range A)) : IsAddStronglyCompleteNatSeq A :=
fun n => (h (Finset.finite_toSet _)).mono (A := .range A \ ((Finset.range n).image A))
(fun _ ⟨⟨y, hy⟩, q⟩ => ⟨y - n, M:Type u_1inst✝¹:AddCommMonoid Minst✝:Preorder MA:ℕ → Mh:IsAddStronglyComplete (Set.range A)n:ℕx✝¹:Mx✝:x✝¹ ∈ Set.range A \ ↑(Finset.image A (Finset.range n))y:ℕhy:A y = x✝¹q:x✝¹ ∉ ↑(Finset.image A (Finset.range n))⊢ (fun m ↦ A (n + m)) (y - n) = x✝¹ All goals completed! 🐙⟩)
If A is strongly complete and the preimage of each element is finite, then the range of A
is strongly complete.
M:Type u_1inst✝¹:AddCommMonoid Minst✝:Preorder MA:ℕ → Mh:IsAddStronglyCompleteNatSeq AhA:∀ (m : M), (A ⁻¹' {m}).FiniteB:Set MhB:B.Finiten:ℕhn:A ⁻¹' B ⊆ Set.Iio nx:Mx✝:x ∈ Set.range fun m ↦ A (n + 1 + m)y:ℕhy:(fun m ↦ A (n + 1 + m)) y = xhx:x ∈ Bthis:n + 1 + y ∈ Set.Iio n⊢ False
All goals completed! 🐙
A sequence A is complete if every sufficiently large element of M is a sum of
(not necessarily distinct) terms of A.
def IsAddCompleteNatSeq' (A : ℕ → M) : Prop :=
∀ᶠ k in Filter.atTop, k ∈ subseqSums' ASequences whose partial sums are dominated by the next term
If A : ℕ → ℕ is strictly increasing from index n₀ on and A 0 + ⋯ + A (m - 1) ≤ A (m + 1)
for m ≥ n₀, then removing infinitely many terms from A destroys completeness. This is the
argument of Graham [Gr64d] for the sequence n ↦ fib n - (-1) ^ n: once three terms
A m₁ < A m₂ < A m are removed, the remaining terms below A (m + 1) sum to at most
A (m + 1) - 2, so A (m + 1) - 1 is not a sum of distinct remaining terms.
Let A : ℕ → ℕ be strictly increasing from index n₀ on, with
A 0 + ⋯ + A (m - 1) ≤ A (m + 1) for all m ≥ n₀. Then Set.range A \ B is not complete for
any infinite B ⊆ Set.range A.