Compositions with an odd number of parts
DefinitionThe index set \(S(m, n, q)\)#✓fully proved
For natural numbers \(m\), \(n\) and \(q\), the set \(S(m, n, q)\) consists of the natural numbers \(k\) such that \(2k \equiv n - q \pmod{m}\), where the difference \(n - q\) is taken in the integers, and \(2k < n\).
For natural numbers the bound \(2k < n\) is equivalent to \(k \le \lfloor (n - 1)/2 \rfloor\); in particular the set is empty when \(n = 0\).
public def compositionHalfIndexSet (m n q : ℕ) : Set ℕ :=
{k | 2 * (k : ℤ) ≡ (n : ℤ) - (q : ℤ) [ZMOD (m : ℤ)] ∧ 2 * k < n}
Sources
- Bowman, Compositions with an Odd Number of Parts, and Other Congruences, Journal of Integer Sequences 27 (2024), Article 24.3.6, Theorem 13 (
jis-2024-24.3.6-thm-13).
TheoremMembership in \(S(m, n, q)\)#✓fully proved
For natural numbers \(m\), \(n\), \(q\) and \(k\), the number \(k\) lies in the index set \(S(m, n, q)\) if and only if \(2k \equiv n - q \pmod{m}\), with the difference taken in the integers, and \(2k < n\).
public theorem mem_compositionHalfIndexSet {m n q k : ℕ} :
k ∈ compositionHalfIndexSet m n q ↔
2 * (k : ℤ) ≡ (n : ℤ) - (q : ℤ) [ZMOD (m : ℤ)] ∧ 2 * k < n
public def compositionHalfIndexSet (m n q : ℕ) : Set ℕ :=
{k | 2 * (k : ℤ) ≡ (n : ℤ) - (q : ℤ) [ZMOD (m : ℤ)] ∧ 2 * k < n}
MathlibExt/Combinatorics/Enumerative/CompositionIndexSets.lean:26
Sources
- Bowman, Compositions with an Odd Number of Parts, and Other Congruences, Journal of Integer Sequences 27 (2024), Article 24.3.6, Theorem 13 (
jis-2024-24.3.6-thm-13).
Uses 1 · Used by 2
TheoremThe index set \(S(m, 0, q)\) is empty#✓fully proved
For all natural numbers \(m\) and \(q\), the index set \(S(m, 0, q)\) is empty.
public theorem compositionHalfIndexSet_zero (m q : ℕ) :
compositionHalfIndexSet m 0 q = ∅
public def compositionHalfIndexSet (m n q : ℕ) : Set ℕ :=
{k | 2 * (k : ℤ) ≡ (n : ℤ) - (q : ℤ) [ZMOD (m : ℤ)] ∧ 2 * k < n}
MathlibExt/Combinatorics/Enumerative/CompositionIndexSets.lean:26
Sources
- Bowman, Compositions with an Odd Number of Parts, and Other Congruences, Journal of Integer Sequences 27 (2024), Article 24.3.6, Theorem 13 (
jis-2024-24.3.6-thm-13).
Uses 2
DefinitionThe index set \(T(m, n, q)\)#✓fully proved
For natural numbers \(m\), \(n\) and \(q\), the set \(T(m, n, q)\) consists of the natural numbers \(k\) such that \(k \equiv n - q \pmod{m}\), where the difference \(n - q\) is taken in the integers, and \(k < n\).
public def compositionIndexSet (m n q : ℕ) : Set ℕ :=
{k | (k : ℤ) ≡ (n : ℤ) - (q : ℤ) [ZMOD (m : ℤ)] ∧ k < n}
Sources
- Bowman, Compositions with an Odd Number of Parts, and Other Congruences, Journal of Integer Sequences 27 (2024), Article 24.3.6, Theorem 17 (
jis-2024-24.3.6-thm-17).
TheoremMembership in \(T(m, n, q)\)#✓fully proved
For natural numbers \(m\), \(n\), \(q\) and \(k\), the number \(k\) lies in the index set \(T(m, n, q)\) if and only if \(k \equiv n - q \pmod{m}\), with the difference taken in the integers, and \(k < n\).
public theorem mem_compositionIndexSet {m n q k : ℕ} :
k ∈ compositionIndexSet m n q ↔
(k : ℤ) ≡ (n : ℤ) - (q : ℤ) [ZMOD (m : ℤ)] ∧ k < n
public def compositionIndexSet (m n q : ℕ) : Set ℕ :=
{k | (k : ℤ) ≡ (n : ℤ) - (q : ℤ) [ZMOD (m : ℤ)] ∧ k < n}
MathlibExt/Combinatorics/Enumerative/CompositionIndexSets.lean:58
Sources
- Bowman, Compositions with an Odd Number of Parts, and Other Congruences, Journal of Integer Sequences 27 (2024), Article 24.3.6, Theorem 17 (
jis-2024-24.3.6-thm-17).
Uses 1 · Used by 2
TheoremThe index set \(T(m, 0, q)\) is empty#✓fully proved
For all natural numbers \(m\) and \(q\), the index set \(T(m, 0, q)\) is empty.
public theorem compositionIndexSet_zero (m q : ℕ) :
compositionIndexSet m 0 q = ∅
public def compositionIndexSet (m n q : ℕ) : Set ℕ :=
{k | (k : ℤ) ≡ (n : ℤ) - (q : ℤ) [ZMOD (m : ℤ)] ∧ k < n}
MathlibExt/Combinatorics/Enumerative/CompositionIndexSets.lean:58
Sources
- Bowman, Compositions with an Odd Number of Parts, and Other Congruences, Journal of Integer Sequences 27 (2024), Article 24.3.6, Theorem 17 (
jis-2024-24.3.6-thm-17).
Uses 2
TheoremDoubling identity for the composition index sets#✓fully proved
For natural numbers \(m\), \(n\) and \(q\), let \(S(m, n, q)\) be the set of natural numbers \(k\) with \(2k \equiv n - q \pmod{m}\) and \(2k < n\), and let \(T(m, n, q)\) be the set of natural numbers \(k\) with \(k \equiv n - q \pmod{m}\) and \(k < n\), where the difference \(n - q\) is taken in the integers. Then for all natural numbers \(m\), \(n\) and \(q\) the sets satisfy \(S(2m, 2n, 2q) = T(m, n, q)\).
public theorem compositionHalfIndexSet_double (m n q : ℕ) :
compositionHalfIndexSet (2 * m) (2 * n) (2 * q)
= compositionIndexSet m n q
public def compositionHalfIndexSet (m n q : ℕ) : Set ℕ :=
{k | 2 * (k : ℤ) ≡ (n : ℤ) - (q : ℤ) [ZMOD (m : ℤ)] ∧ 2 * k < n}
MathlibExt/Combinatorics/Enumerative/CompositionIndexSets.lean:26
public def compositionIndexSet (m n q : ℕ) : Set ℕ :=
{k | (k : ℤ) ≡ (n : ℤ) - (q : ℤ) [ZMOD (m : ℤ)] ∧ k < n}
MathlibExt/Combinatorics/Enumerative/CompositionIndexSets.lean:58
Sources
- Bowman, Compositions with an Odd Number of Parts, and Other Congruences, Journal of Integer Sequences 27 (2024), Article 24.3.6, Lemma 18 (
jis-2024-24.3.6-lem-18).
Uses 4
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.