Bounds on the partition function

TheoremBijection removing \(k\) copies of a part from partitions#✓fully proved

Removing k copies of the positive part v gives a bijection from partitions of E containing at least k copies of v to partitions of E - k * v.

theorem card_count_ge {E v k : ℕ} (hv : 1 ≤ v) (hkv : k * v ≤ E) :
    Fintype.card {p : Partition E // k ≤ p.parts.count v} =
      Fintype.card (Partition (E - k * v))

Used by 2

Used byMonotonicity of the partition function · Sum-of-parts recurrence for the partition function

TheoremMonotonicity of the partition function#✓fully proved

The number of integer partitions is monotone in the integer being partitioned.

theorem card_monotone : Monotone fun E => Fintype.card (Partition E)

Uses 1

Proof usesBijection removing \(k\) copies of a part from partitions

TheoremSum-of-parts recurrence for the partition function#✓fully proved

A recurrence obtained by summing all parts of all partitions of E, first by partition and then by part value and multiplicity threshold.

theorem mul_card_eq_sum (E : ℕ) :
    E * Fintype.card (Partition E) =
      ∑ v ∈ Icc 1 E, ∑ k ∈ Icc 1 (E / v),
        v * Fintype.card (Partition (E - k * v))

Uses 1 · Used by 3

Proof usesBijection removing \(k\) copies of a part from partitions

Used byExponential upper bound for the partition function · Exponential lower bound for the partition function · Linear lower bound for the partition function

TheoremExponential lower bound for the partition function#✓fully proved

The number of partitions of n is at least H * exp (pi * sqrt (2 / 3) * sqrt n) / n ^ B for some H > 0 and natural B, when n ≥ 1.

theorem exists_exp_div_pow_le_card :
    ∃ (H : ℝ) (B : ℕ), 0 < H ∧ ∀ n : ℕ, 1 ≤ n →
      H * Real.exp (Real.pi * Real.sqrt ((2 : ℝ) / 3) * Real.sqrt n) / (n : ℝ) ^ B ≤
        (Fintype.card (Partition n) : ℝ)

Uses 1 · Used by 1

Proof usesSum-of-parts recurrence for the partition function

Used byLogarithmic bounds for the partition function

TheoremExponential upper bound for the partition function#✓fully proved

The number of integer partitions of n is at most exp (π * sqrt (2 / 3) * sqrt n).

theorem card_le_exp (n : ℕ) :
    (Fintype.card (Partition n) : ℝ) ≤
      Real.exp (Real.pi * Real.sqrt ((2 : ℝ) / 3) * Real.sqrt n)

Uses 1 · Used by 1

Proof usesSum-of-parts recurrence for the partition function

Used byLogarithmic bounds for the partition function

TheoremLinear lower bound for the partition function#✓fully proved

The number of partitions of n is at least (n + 1) / 2.

theorem succ_le_two_mul_card (n : ℕ) :
    n + 1 ≤ 2 * Fintype.card (Partition n)

Uses 1

Proof usesSum-of-parts recurrence for the partition function

TheoremLogarithmic bounds for the partition function#✓fully proved

There are constants B and C such that the base-two logarithm of the number of integer partitions of n differs from its leading square-root term by at most a logarithmic lower-order term below and a constant above.

theorem exists_logb_card_bounds :
    ∃ B C : ℝ,
      (∀ n : ℕ, 1 ≤ n →
        (Real.pi * Real.sqrt ((2 : ℝ) / 3) / Real.log 2) * Real.sqrt n -
              B * Real.logb 2 (n : ℝ) - C ≤
            Real.logb 2 (Fintype.card (Partition n) : ℝ)) ∧
      (∀ n : ℕ,
        Real.logb 2 (Fintype.card (Partition n) : ℝ) ≤
          (Real.pi * Real.sqrt ((2 : ℝ) / 3) / Real.log 2) * Real.sqrt n + C)

Uses 2

Proof usesExponential upper bound for the partition function · Exponential lower bound for the partition function

7 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.