Van der Laan sequences

DefinitionVan der Laan windows#✓fully proved

Four natural numbers \(a, b, c, d\) form a Van der Laan window when the largest of them equals the sum of the two smallest, that is, when \(\max(a, b, c, d) = \min(a + b, a + c, a + d, b + c, b + d, c + d)\).

The minimum of the six pair sums is the sum of the two smallest of the four values counted with multiplicity, so repeated values are handled correctly.

public def IsVanDerLaanWindow (a b c d : ℕ) : Prop :=
  max (max a b) (max c d)
    = min (min (a + b) (a + c)) (min (min (a + d) (b + c)) (min (b + d) (c + d)))

Used by 4

Used byVan der Laan sequences · Constant Van der Laan sequences · Constant Van der Laan windows · Van der Laan windows in increasing order

DefinitionVan der Laan sequences#✓fully proved

A sequence \(s \colon \mathbb{N} \to \mathbb{N}\) is a Van der Laan sequence when, for every \(n \in \mathbb{N}\), the four consecutive terms \(s(n), s(n + 1), s(n + 2), s(n + 3)\) form a Van der Laan window, that is, the largest of them equals the sum of the two smallest.

public def IsVanDerLaan (s : ℕ → ℕ) : Prop :=
  ∀ n : ℕ, IsVanDerLaanWindow (s n) (s (n + 1)) (s (n + 2)) (s (n + 3))

public def IsVanDerLaanWindow (a b c d : ℕ) : Prop :=
  max (max a b) (max c d)
    = min (min (a + b) (a + c)) (min (min (a + d) (b + c)) (min (b + d) (c + d)))

MathlibExt/Combinatorics/VanDerLaanSequence.lean:30

Uses 1 · Used by 1

Statement usesVan der Laan windows

Used byConstant Van der Laan sequences

TheoremVan der Laan windows in increasing order#✓fully proved

Let \(a \le b \le c \le d\) be natural numbers. Then \(a, b, c, d\) form a Van der Laan window if and only if \(d = a + b\).

public theorem isVanDerLaanWindow_ordered_iff {a b c d : ℕ} (hab : a ≤ b) (hbc : b ≤ c)
    (hcd : c ≤ d) : IsVanDerLaanWindow a b c d ↔ d = a + b

public def IsVanDerLaanWindow (a b c d : ℕ) : Prop :=
  max (max a b) (max c d)
    = min (min (a + b) (a + c)) (min (min (a + d) (b + c)) (min (b + d) (c + d)))

MathlibExt/Combinatorics/VanDerLaanSequence.lean:30

Uses 1

Statement usesVan der Laan windows

TheoremConstant Van der Laan windows#✓fully proved

For a natural number \(k\), the window \(k, k, k, k\) is a Van der Laan window if and only if \(k = 0\).

Its largest value is \(k\) and the sum of its two smallest values is \(k + k\).

public theorem isVanDerLaanWindow_const_iff {k : ℕ} :
    IsVanDerLaanWindow k k k k ↔ k = 0

public def IsVanDerLaanWindow (a b c d : ℕ) : Prop :=
  max (max a b) (max c d)
    = min (min (a + b) (a + c)) (min (min (a + d) (b + c)) (min (b + d) (c + d)))

MathlibExt/Combinatorics/VanDerLaanSequence.lean:30

Uses 1 · Used by 1

Statement usesVan der Laan windows

Used byConstant Van der Laan sequences

TheoremConstant Van der Laan sequences#✓fully proved

For a natural number \(k\), the constant sequence \(s \colon \mathbb{N} \to \mathbb{N}\) with \(s(n) = k\) for all \(n\) is a Van der Laan sequence if and only if \(k = 0\).

In particular the identically zero sequence, one of the alternatives in the source conjecture, is a Van der Laan sequence.

public theorem isVanDerLaan_const_iff {k : ℕ} :
    IsVanDerLaan (fun _ => k) ↔ k = 0

Uses 3

Statement usesVan der Laan sequences

Proof usesVan der Laan windows · Constant Van der Laan windows

5 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.