Overpartitions

15 fully proved

Overpartition

StructureOverpartition#✓fully proved

An overpartition of a natural number \(n\) consists of a partition \(p\) of \(n\) together with a finite set of overlined part sizes, each of which occurs as a part of \(p\).

@[ext]
structure Overpartition (n : ℕ) where
  /-- The underlying partition. -/
  toPartition : Partition n
  /-- The distinct part sizes that are overlined. -/
  overlines : Finset ℕ
  /-- Every overlined size occurs in the underlying partition. -/
  overlines_subset : overlines ⊆ toPartition.parts.toFinset
deriving DecidableEq

Used by 36

Used byMinimal excludant of an overpartition with a multiplicity bound · Number of non-overlined copies of a part size · Number of overpartitions · The number of overpartitions of zero · Sums of minimal excludants over overpartitions · Overpartitions into odd parts from overpartitions and squares · Overpartitions of even numbers into odd parts · Overpartitions of odd numbers into odd parts · Overpartitions into odd parts · Overpartitions of zero into odd parts · Uniqueness of the overpartition of zero · Fully overlined overpartition · Overlined sizes of the fully overlined overpartition · Underlying partition of the fully overlined overpartition · Overlined part size · Characterization of overlined sizes · Overlined sizes are parts · Overlined sizes are positive · The overpartition attached to a partition · The overpartition attached to a partition has no overlined sizes · The underlying partition of the overpartition attached to a partition · Overpartitions of zero have no overlined sizes · Overpartitions as pairs of a multiset and a set · Overpartitions of \(5n\) modulo \(5\) · Liang's congruences modulo 512 for overpartitions · Number of \(\ell\)-regular overpartitions · Two \(\ell\)-regular overpartitions of one · One \(\ell\)-regular overpartition of zero · Number of smallest even parts in overpartitions · Smallest-even-part contribution of an overpartition · Overpartitions with odd smallest part contribute nothing · \(\overline{\mathrm{spt2}}\) vanishes at zero · Glaisher's divisor functions as series-divisors · Recurrences for partitions into even or distinct parts and for overpartitions · Overpartition formulas for a divisor sum with odd cofactors · Overpartitions modulo \(8\) and a convolution of divisor sums

DefinitionOverlined part size#✓fully proved

A natural number \(a\) is overlined in an overpartition \(O\) of \(n\) when \(a\) belongs to the set of overlined part sizes of \(O\).

def IsOverlined {n : ℕ} (O : Overpartition n) (a : ℕ) : Prop :=
  a ∈ O.overlines

Uses 1 · Used by 5

Statement usesOverpartition

Used byOverlined sizes in the fully overlined overpartition · Characterization of overlined sizes · Overlined sizes are parts · Overlined sizes are positive · No overlines in a plain partition

TheoremCharacterization of overlined sizes#✓fully proved

For an overpartition \(O\) of \(n\) and a natural number \(a\), \(a\) is overlined in \(O\) if and only if \(a\) belongs to the set of overlined part sizes of \(O\).

theorem isOverlined_iff {n : ℕ} {O : Overpartition n} {a : ℕ} :
    O.IsOverlined a ↔ a ∈ O.overlines

Uses 2

Statement usesOverpartition · Overlined part size

TheoremOverlined sizes are parts#✓fully proved

If \(a\) is overlined in an overpartition \(O\) of \(n\), then \(a\) is a part of the underlying partition of \(O\).

theorem isOverlined_mem_parts {n : ℕ} {O : Overpartition n} {a : ℕ}
    (h : O.IsOverlined a) : a ∈ O.toPartition.parts

Uses 2 · Used by 1

Statement usesOverpartition · Overlined part size

Used byOverlined sizes are positive

TheoremOverlined sizes are positive#✓fully proved

If \(a\) is overlined in an overpartition \(O\) of \(n\), then \(a > 0\).

theorem isOverlined_pos {n : ℕ} {O : Overpartition n} {a : ℕ}
    (h : O.IsOverlined a) : 0 < a

Uses 3

Statement usesOverpartition · Overlined part size

Proof usesOverlined sizes are parts

DefinitionThe overpartition attached to a partition#✓fully proved

For a partition \(p\) of a natural number \(n\), the overpartition of \(n\) attached to \(p\) has underlying partition \(p\) and no overlined part sizes.

def ofPartition {n : ℕ} (p : Partition n) : Overpartition n where
  toPartition := p
  overlines := ∅
  overlines_subset := by simp

Uses 1 · Used by 6

Statement usesOverpartition

Used byThe number of overpartitions of zero · Overpartitions of zero into odd parts · No overlines in a plain partition · The overpartition attached to a partition has no overlined sizes · The underlying partition of the overpartition attached to a partition · One \(\ell\)-regular overpartition of zero

TheoremThe underlying partition of the overpartition attached to a partition#✓fully proved

For every partition \(p\) of a natural number \(n\), the underlying partition of the overpartition of \(n\) attached to \(p\) (underlying partition \(p\), no part size overlined) is \(p\).

@[simp]
theorem ofPartition_toPartition {n : ℕ} (p : Partition n) :
    (ofPartition p).toPartition = p

Uses 2

Statement usesOverpartition · The overpartition attached to a partition

TheoremThe overpartition attached to a partition has no overlined sizes#✓fully proved

For every partition \(p\) of a natural number \(n\), the overpartition of \(n\) attached to \(p\) (underlying partition \(p\), no part size overlined) has an empty set of overlined part sizes.

@[simp]
theorem ofPartition_overlines {n : ℕ} (p : Partition n) :
    (ofPartition p).overlines = ∅

Uses 2

Statement usesOverpartition · The overpartition attached to a partition

TheoremNo overlines in a plain partition#✓fully proved

For every partition \(p\) of \(n\) and every natural number \(a\), \(a\) is not overlined in the overpartition whose underlying partition is \(p\) and whose set of overlined part sizes is empty.

@[simp]
theorem not_isOverlined_ofPartition {n : ℕ} (p : Partition n) (a : ℕ) :
    ¬ (ofPartition p).IsOverlined a

Uses 2

Statement usesOverlined part size · The overpartition attached to a partition

DefinitionFully overlined overpartition#✓fully proved

For a partition \(p\) of \(n\), the fully overlined overpartition of \(p\) is the overpartition of \(n\) whose underlying partition is \(p\) and whose set of overlined part sizes is the set of all distinct parts of \(p\).

def full {n : ℕ} (p : Partition n) : Overpartition n where
  toPartition := p
  overlines := p.parts.toFinset
  overlines_subset := fun _ hx => hx

Uses 1 · Used by 3

Statement usesOverpartition

Used byOverlined sizes of the fully overlined overpartition · Underlying partition of the fully overlined overpartition · Overlined sizes in the fully overlined overpartition

TheoremUnderlying partition of the fully overlined overpartition#✓fully proved

For every partition \(p\) of \(n\), the underlying partition of the fully overlined overpartition of \(p\) is \(p\).

@[simp]
theorem full_toPartition {n : ℕ} (p : Partition n) :
    (full p).toPartition = p

Uses 2

Statement usesOverpartition · Fully overlined overpartition

TheoremOverlined sizes of the fully overlined overpartition#✓fully proved

For every partition \(p\) of \(n\), the set of overlined part sizes of the fully overlined overpartition of \(p\) is the set of distinct parts of \(p\).

@[simp]
theorem full_overlines {n : ℕ} (p : Partition n) :
    (full p).overlines = p.parts.toFinset

Uses 2

Statement usesOverpartition · Fully overlined overpartition

TheoremOverlined sizes in the fully overlined overpartition#✓fully proved

For every partition \(p\) of \(n\) and every natural number \(a\), \(a\) is overlined in the fully overlined overpartition of \(p\) if and only if \(a\) is a part of \(p\).

@[simp]
theorem isOverlined_full {n : ℕ} (p : Partition n) (a : ℕ) :
    (full p).IsOverlined a ↔ a ∈ p.parts

Uses 2

Statement usesOverlined part size · Fully overlined overpartition

TheoremOverpartitions of zero have no overlined sizes#✓fully proved

Every overpartition of \(0\) has no overlined part sizes.

theorem overlines_eq_empty_of_zero {O : Overpartition 0} : O.overlines = ∅

Uses 1 · Used by 1

Statement usesOverpartition

Used byUniqueness of the overpartition of zero

TheoremUniqueness of the overpartition of zero#✓fully proved

Any two overpartitions of \(0\) are equal.

theorem eq_of_zero (O₁ O₂ : Overpartition 0) : O₁ = O₂

Uses 2 · Used by 3

Statement usesOverpartition

Proof usesOverpartitions of zero have no overlined sizes

Used byThe number of overpartitions of zero · Overpartitions of zero into odd parts · One \(\ell\)-regular overpartition of zero

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.