/-
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 FormalConjecturesForMathlib.Order.Filter.Cofinite
public import FormalConjecturesForMathlib.Algebra.Group.Action.Pointwise.Set.Basic
public import Mathlib.Algebra.Group.Pointwise.Set.BigOperators
public import Mathlib.Algebra.Group.Pointwise.Set.Finite
public import Mathlib.Algebra.Order.Monoid.Canonical.Defs@[expose] public sectionBases
References:
[Er56](Erdős, P., Problems and results in additive number theory. Colloque sur la Théorie des Nombres, Bruxelles, 1955 (1956), 127-137.)
open Filteropen scoped Pointwisenamespace Setvariable {M : Type*} [CommMonoid M] {A : Set M} {m n : ℕ}
A set A : Set M is a multiplicative basis of order n if any element a : M
can be expressed as a product of n elements lying in A.
@[to_additive
A set A : Set M is an additive basis of order n if for any element
a : M, it can be expressed as a sum of n elements lying in A.
]
def IsMulBasisOfOrder (A : Set M) (n : ℕ) : Prop := ∀ a, a ∈ A ^ nA multiplicative basis of some order.
@[to_additiveAn additive basis of some order.
]
def IsMulBasis (A : Set M) : Prop := ∃ n, A.IsMulBasisOfOrder n@[to_additive]
lemma IsMulBasisOfOrder.isMulBasis (hA : A.IsMulBasisOfOrder n) : A.IsMulBasis := ⟨n, hA⟩@[to_additive]
lemma isMulBasisOfOrder_iff :
A.IsMulBasisOfOrder n ↔ ∀ a, ∃ (f : Fin n → M) (_ : ∀ i, f i ∈ A), ∏ i, f i = a := M:Type u_1inst✝:CommMonoid MA:Set Mn:ℕ⊢ A.IsMulBasisOfOrder n ↔ ∀ (a : M), ∃ f, ∃ (_ : ∀ (i : Fin n), f i ∈ A), ∏ i, f i = a
M:Type u_1inst✝:CommMonoid MA:Set Mn:ℕthis:∀ (a : M), a ∈ ∏ i, A ↔ ∃ g, ∃ (_ : ∀ {i : Fin n}, i ∈ Finset.univ → g i ∈ A), ∏ i, g i = a⊢ A.IsMulBasisOfOrder n ↔ ∀ (a : M), ∃ f, ∃ (_ : ∀ (i : Fin n), f i ∈ A), ∏ i, f i = a
All goals completed! 🐙
No set is a multiplicative basis of order 0.
@[to_additive (attr := simp)
No set is an additive basis of order 0.
]
lemma not_isMulBasisOfOrder_zero [Nontrivial M] : ¬A.IsMulBasisOfOrder 0 := M:Type u_1inst✝¹:CommMonoid MA:Set Minst✝:Nontrivial M⊢ ¬A.IsMulBasisOfOrder 0
All goals completed! 🐙@[to_additive (attr := simp)]
lemma isMulBasisOfOrder_one_iff : A.IsMulBasisOfOrder 1 ↔ A = univ := M:Type u_1inst✝:CommMonoid MA:Set M⊢ A.IsMulBasisOfOrder 1 ↔ A = univ
All goals completed! 🐙
A set A : Set M is a multiplicative basis of order 2 if every a : M belongs to A * A.
@[to_additive
A set A : Set M is an additive basis of order 2 if every a : M belongs to A + A.
]
lemma isMulBasisOfOrder_two_iff : A.IsMulBasisOfOrder 2 ↔ ∀ a, a ∈ A * A := M:Type u_1inst✝:CommMonoid MA:Set M⊢ A.IsMulBasisOfOrder 2 ↔ ∀ (a : M), a ∈ A * A
All goals completed! 🐙
A set A : Set M is an asymptotic multiplicative basis of order n if the elements that can
be expressed as a product of n elements lying in A is cofinite.
@[to_additive
A set A : Set M is an asymptotic additive basis of order n if the elements that
can be expressed as a sum of n elements lying in A is cofinite.
]
def IsAsymptoticMulBasisOfOrder (A : Set M) (n : ℕ) : Prop := ∀ᶠ a in cofinite, a ∈ A ^ nAn asymptotic multiplicative basis of some order.
@[to_additiveAn asymptotic additive basis of some order.
]
def IsAsymptoticMulBasis (A : Set M) : Prop := ∃ n, A.IsAsymptoticMulBasisOfOrder n@[to_additive]
lemma IsAsymptoticMulBasisOfOrder.isAsymptoticMulBasis (hA : A.IsAsymptoticMulBasisOfOrder n) :
A.IsAsymptoticMulBasis := ⟨n, hA⟩@[to_additive]
lemma IsMulBasisOfOrder.isAsymptoticMulBasisOfOrder (hA : IsMulBasisOfOrder A n) :
A.IsAsymptoticMulBasisOfOrder n := .of_forall hA@[to_additive]
lemma IsMulBasis.isAsymptoticMulBasis (hA : IsMulBasis A) : A.IsAsymptoticMulBasis := M:Type u_1inst✝:CommMonoid MA:Set MhA:A.IsMulBasis⊢ A.IsAsymptoticMulBasis
M:Type u_1inst✝:CommMonoid MA:Set Mn:ℕhn:A.IsMulBasisOfOrder n⊢ A.IsAsymptoticMulBasis; All goals completed! 🐙
A set A : Set M is an asymptotic multiplicative basis of order n if a cofinite set of
a : M can be written as a = a₁ * ... * aₙ, where each aᵢ ∈ A.
@[to_additive
A set A : Set M is an asymptotic additive basis of order n if a cofinite set of
a : M can be written as a = a₁ + ... + aₙ, where each aᵢ ∈ A.
]
lemma isAsymptoticMulBasisOfOrder_iff_prod :
IsAsymptoticMulBasisOfOrder A n ↔ ∀ᶠ a in cofinite, ∃ (f : Fin n → M) (_ : ∀ i, f i ∈ A),
∏ i, f i = a := M:Type u_1inst✝:CommMonoid MA:Set Mn:ℕ⊢ A.IsAsymptoticMulBasisOfOrder n ↔ ∀ᶠ (a : M) in cofinite, ∃ f, ∃ (_ : ∀ (i : Fin n), f i ∈ A), ∏ i, f i = a
M:Type u_1inst✝:CommMonoid MA:Set Mn:ℕthis:∀ (a : M), a ∈ ∏ i, A ↔ ∃ g, ∃ (_ : ∀ {i : Fin n}, i ∈ Finset.univ → g i ∈ A), ∏ i, g i = a⊢ A.IsAsymptoticMulBasisOfOrder n ↔ ∀ᶠ (a : M) in cofinite, ∃ f, ∃ (_ : ∀ (i : Fin n), f i ∈ A), ∏ i, f i = a
All goals completed! 🐙
A set A : Set M is an asymptotic multiplicative basis of order 2 if a cofinite set of
a : M belongs to A * A.
@[to_additive
A set A : Set M is an asymptotic additive basis of order 2 if a cofinite set of
a : M belongs to A + A.
]
lemma isAsymptoticMulBasisOfOrder_two_iff :
IsAsymptoticMulBasisOfOrder A 2 ↔ ∀ᶠ a in cofinite, a ∈ A * A := M:Type u_1inst✝:CommMonoid MA:Set M⊢ A.IsAsymptoticMulBasisOfOrder 2 ↔ ∀ᶠ (a : M) in cofinite, a ∈ A * A
All goals completed! 🐙@[to_additive (attr := simp)]
protected lemma IsAsymptoticMulBasisOfOrder.of_finite [Finite M] :
IsAsymptoticMulBasisOfOrder A n := M:Type u_1inst✝¹:CommMonoid MA:Set Mn:ℕinst✝:Finite M⊢ A.IsAsymptoticMulBasisOfOrder n All goals completed! 🐙
If M is infinite, then no set A is an asymptotic multiplicative basis of order 0.
@[to_additive (attr := simp)
If M is infinite, then no set A is an asymptotic additive basis of order 0.
]
lemma not_isAsymptoticMulBasisOfOrder_zero [Infinite M] : ¬IsAsymptoticMulBasisOfOrder A 0 := M:Type u_1inst✝¹:CommMonoid MA:Set Minst✝:Infinite M⊢ ¬A.IsAsymptoticMulBasisOfOrder 0
simpa [IsAsymptoticMulBasisOfOrder, ← not_infinite] using Set.infinite_of_finite_compl (M:Type u_1inst✝¹:CommMonoid MA:Set Minst✝:Infinite M⊢ {x | ¬x = 1}ᶜ.Finite All goals completed! 🐙)@[to_additive]
protected lemma IsAsymptoticMulBasisOfOrder.ne_zero [Infinite M]
(hA : IsAsymptoticMulBasisOfOrder A n) : n ≠ 0 := M:Type u_1inst✝¹:CommMonoid MA:Set Mn:ℕinst✝:Infinite MhA:A.IsAsymptoticMulBasisOfOrder n⊢ n ≠ 0 M:Type u_1inst✝¹:CommMonoid MA:Set Minst✝:Infinite MhA:A.IsAsymptoticMulBasisOfOrder 0⊢ False; All goals completed! 🐙@[to_additive]
protected lemma IsAsymptoticMulBasisOfOrder.nonempty [Infinite M]
(hA : A.IsAsymptoticMulBasisOfOrder n) : A.Nonempty := M:Type u_1inst✝¹:CommMonoid MA:Set Mn:ℕinst✝:Infinite MhA:A.IsAsymptoticMulBasisOfOrder n⊢ A.Nonempty
M:Type u_1inst✝¹:CommMonoid MA:Set Mn:ℕinst✝:Infinite MhA:A.IsAsymptoticMulBasisOfOrder nthis:A = ∅⊢ False
All goals completed! 🐙
A : Set M is an asymptotic basis of order one iff it is cofinite.
@[to_additive (attr := simp)
A : Set M is an asymptotic basis of order one iff it is cofinite.
]
lemma isAsymptoticMulBasisOfOrder_one_iff : IsAsymptoticMulBasisOfOrder A 1 ↔ Aᶜ.Finite := M:Type u_1inst✝:CommMonoid MA:Set M⊢ A.IsAsymptoticMulBasisOfOrder 1 ↔ Aᶜ.Finite
All goals completed! 🐙variable [LinearOrder M] [LocallyFiniteOrder M] [OrderBot M]M:Type u_1inst✝⁵:CommMonoid MA:Set Mm:ℕinst✝⁴:LinearOrder Minst✝³:LocallyFiniteOrder Minst✝²:OrderBot Minst✝¹:CanonicallyOrderedMul Minst✝:IsCancelMul MhA:A.IsAsymptoticMulBasisOfOrder mh✝:Infinite Ma:Mha:a ∈ An:ℕhmn:m ≤ m + nthis:a ^ n • (A ^ m)ᶜ = (a ^ n • A ^ m)ᶜ \ Iio (a ^ n)⊢ {x | (fun a ↦ a ∈ A ^ (m + n)) x}ᶜ ⊆ a ^ n • {x | (fun a ↦ a ∈ A ^ m) x}ᶜ ∪ Iio (a ^ n)
M:Type u_1inst✝⁵:CommMonoid MA:Set Mm:ℕinst✝⁴:LinearOrder Minst✝³:LocallyFiniteOrder Minst✝²:OrderBot Minst✝¹:CanonicallyOrderedMul Minst✝:IsCancelMul MhA:A.IsAsymptoticMulBasisOfOrder mh✝:Infinite Ma:Mha:a ∈ An:ℕhmn:m ≤ m + nthis:a ^ n • (A ^ m)ᶜ = (a ^ n • A ^ m)ᶜ \ Iio (a ^ n)⊢ ∀ x ∉ A ^ n * A ^ m, x ∉ a ^ n • A ^ m ∨ x < a ^ n
M:Type u_1inst✝⁵:CommMonoid MA:Set Mm:ℕinst✝⁴:LinearOrder Minst✝³:LocallyFiniteOrder Minst✝²:OrderBot Minst✝¹:CanonicallyOrderedMul Minst✝:IsCancelMul MhA:A.IsAsymptoticMulBasisOfOrder mh✝:Infinite Ma:Mha:a ∈ An:ℕhmn:m ≤ m + nthis:a ^ n • (A ^ m)ᶜ = (a ^ n • A ^ m)ᶜ \ Iio (a ^ n)b:Mhb:b ∉ A ^ n * A ^ m⊢ b ∉ a ^ n • A ^ m ∨ b < a ^ n
M:Type u_1inst✝⁵:CommMonoid MA:Set Mm:ℕinst✝⁴:LinearOrder Minst✝³:LocallyFiniteOrder Minst✝²:OrderBot Minst✝¹:CanonicallyOrderedMul Minst✝:IsCancelMul MhA:A.IsAsymptoticMulBasisOfOrder mh✝:Infinite Ma:Mha:a ∈ An:ℕhmn:m ≤ m + nthis:a ^ n • (A ^ m)ᶜ = (a ^ n • A ^ m)ᶜ \ Iio (a ^ n)b:Mhb:b ∈ a ^ n • A ^ m ∧ a ^ n ≤ b⊢ b ∈ A ^ n * A ^ m
All goals completed! 🐙
For M equipped with a directed order, a set is an asymptotic multiplicative basis of order 1
if it contains an infinite tail of elements.
@[to_additive
For M equipped with a directed order, a set is an asymptotic additive basis of order 1
if it contains an infinite tail of consecutive naturals.
]
lemma isAsymptoticMulBasisOfOrder_one_iff_Ioi :
IsAsymptoticMulBasisOfOrder A 1 ↔ ∃ a, .Ioi a ⊆ A := M:Type u_1inst✝³:CommMonoid MA:Set Minst✝²:LinearOrder Minst✝¹:LocallyFiniteOrder Minst✝:OrderBot M⊢ A.IsAsymptoticMulBasisOfOrder 1 ↔ ∃ a, Ioi a ⊆ A
All goals completed! 🐙variable [SuccOrder M] [NoMaxOrder M]
For M equipped with a directed order, a set is an asymptotic multiplicative basis of order 1
if it contains an infinite tail of elements.
@[to_additive
For M equipped with a directed order, a set is an asymptotic additive basis of order 1
if it contains an infinite tail of consecutive naturals.
]
lemma isAsymptoticMulBasisOfOrder_one_iff_Ici :
IsAsymptoticMulBasisOfOrder A 1 ↔ ∃ a, .Ici a ⊆ A := M:Type u_1inst✝⁵:CommMonoid MA:Set Minst✝⁴:LinearOrder Minst✝³:LocallyFiniteOrder Minst✝²:OrderBot Minst✝¹:SuccOrder Minst✝:NoMaxOrder M⊢ A.IsAsymptoticMulBasisOfOrder 1 ↔ ∃ a, Ici a ⊆ A
All goals completed! 🐙All goals completed! 🐙@[to_additive]
lemma isAsymptoticMulBasisOfOrder_iff_prod_atTop :
IsAsymptoticMulBasisOfOrder A n ↔
∀ᶠ a in atTop, ∃ f : Fin n → M, (∀ i, f i ∈ A) ∧ ∏ i, f i = a := M:Type u_1inst✝⁵:CommMonoid MA:Set Mn:ℕinst✝⁴:LinearOrder Minst✝³:LocallyFiniteOrder Minst✝²:OrderBot Minst✝¹:SuccOrder Minst✝:NoMaxOrder M⊢ A.IsAsymptoticMulBasisOfOrder n ↔ ∀ᶠ (a : M) in atTop, ∃ f, (∀ (i : Fin n), f i ∈ A) ∧ ∏ i, f i = a
All goals completed! 🐙
A set A : Set M is a weak multiplicative basis of order n if any element a : M
can be expressed as a product of at most n elements lying in A.
@[to_additive
A set A : Set M is a weak additive basis of order n if for any element
a : M, it can be expressed as a sum of at most n elements lying in A.
]
def IsWeakMulBasisOfOrder (A : Set M) (n : ℕ) : Prop := ∀ a, ∃ m ≤ n, a ∈ A ^ mA weak multiplicative basis of some order.
@[to_additiveA weak additive basis of some order.
]
def IsWeakMulBasis (A : Set M) : Prop := ∃ n, A.IsWeakMulBasisOfOrder nend Set