Landau's function

4 fully proved

Partition

DefinitionLeast common multiple of the parts of a partition#✓fully proved

For a natural number \(n\) and a partition \(p\) of \(n\), this is the least common multiple of the parts of \(p\), taken with the convention that it equals \(1\) when \(p\) has no parts.

def partsLCM {n : ℕ} (p : n.Partition) : ℕ :=
  p.parts.lcm

Used by 3

Used byThe Landau function is attained · Landau's function · The Landau function bounds the LCM of the parts

Landau's function

DefinitionLandau's function#✓fully proved

For a natural number \(n\), Landau's function at \(n\) is the maximum, over all partitions \(p\) of \(n\), of the least common multiple of the parts of \(p\).

def landauFunction (n : ℕ) : ℕ :=
  Finset.univ.sup (fun p : n.Partition => p.partsLCM)

Uses 1 · Used by 2

Statement usesLeast common multiple of the parts of a partition

Used byThe Landau function is attained · The Landau function bounds the LCM of the parts

TheoremThe Landau function bounds the LCM of the parts#✓fully proved

For every natural number \(n\) and every partition \(p\) of \(n\), the least common multiple of the parts of \(p\) is at most the Landau function at \(n\).

theorem Partition.partsLCM_le_landauFunction {n : ℕ} (p : n.Partition) :
    p.partsLCM ≤ landauFunction n

Uses 2

Statement usesLeast common multiple of the parts of a partition · Landau's function

TheoremThe Landau function is attained#✓fully proved

For every natural number \(n\), some partition of \(n\) has least common multiple of its parts equal to the Landau function at \(n\).

theorem exists_partition_partsLCM_eq_landauFunction (n : ℕ) :
    ∃ p : n.Partition, p.partsLCM = landauFunction n

Uses 2

Statement usesLeast common multiple of the parts of a partition · Landau's function

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.