Taylor's law for integer sequences

DefinitionAdmissible sequences for Taylor's law#✓fully proved

A sequence \(a : \mathbb{N} \to \mathbb{N}\), indexed from \(1\) (its value at \(0\) is ignored), is admissible when \(a(n) > 0\) for every \(n \ge 1\) and there is \(n_0 \ge 1\) such that \(a(n) < a(n + 1)\) for every \(n \ge n_0\).

public def IsTaylorAdmissibleSequence (a : ℕ → ℕ) : Prop :=
  (∀ n, 0 < n → 0 < a n) ∧ ∃ n₀, 1 ≤ n₀ ∧ ∀ n, n₀ ≤ n → a n < a (n + 1)

Sources

• Joel E. Cohen, Variance Functions of Asymptotically Exponentially Increasing Integer Sequences Go Beyond Taylor's Law, Journal of Integer Sequences 25 (2022), Article 22.9.3, the collection 𝒜 of infinite eventually strictly increasing sequences of natural numbers, lines 113–125, https://cs.uwaterloo.ca/journals/JIS/VOL25/Cohen/cohen13.tex.

Used by 1

Used byTaylor's law, asymptotic form

DefinitionInitial-segment mean#✓fully proved

For a sequence \(a : \mathbb{N} \to \mathbb{N}\) and \(n \in \mathbb{N}\), the initial-segment mean is the real number \(m(a, n) = \frac{1}{n} \sum_{j=1}^{n} a(j)\), with the convention \(1 / 0 = 0\), so that \(m(a, 0) = 0\).

The source uses \(m(a, n)\) only for \(n \ge 2\), with indices starting at \(1\).

noncomputable def initialSegmentMean (a : ℕ → ℕ) (n : ℕ) : ℝ :=
  (1 / (n : ℝ)) * ∑ j ∈ Finset.range n, (a (j + 1) : ℝ)

Sources

• Joel E. Cohen, Variance Functions of Asymptotically Exponentially Increasing Integer Sequences Go Beyond Taylor's Law, Journal of Integer Sequences 25 (2022), Article 22.9.3, mean/variance definitions, lines 119–124, equation eq:mean at line 122, https://cs.uwaterloo.ca/journals/JIS/VOL25/Cohen/cohen13.tex.

Used by 1

Used byTaylor's law, asymptotic form

DefinitionInitial-segment sample variance#✓fully proved

For a sequence \(a : \mathbb{N} \to \mathbb{N}\) and \(n \in \mathbb{N}\), the unbiased initial-segment sample variance is the real number \(v(a, n) = \frac{1}{n - 1} \sum_{j=1}^{n} \left(a(j) - \frac{1}{n} \sum_{k=1}^{n} a(k)\right)^2\), with the convention \(1 / 0 = 0\); in particular \(v(a, 0) = v(a, 1) = 0\).

The inner average is the initial-segment mean \(m(a, n)\). The source uses \(v(a, n)\) only for \(n \ge 2\), with indices starting at \(1\).

noncomputable def initialSegmentSampleVariance (a : ℕ → ℕ) (n : ℕ) : ℝ :=
  ((n : ℝ) - 1)⁻¹ * ∑ j ∈ Finset.Icc 1 n,
    (((a j : ℝ) - (1 / (n : ℝ)) * ∑ k ∈ Finset.Icc 1 n, (a k : ℝ)) ^ 2)

Sources

• Joel E. Cohen, Variance Functions of Asymptotically Exponentially Increasing Integer Sequences Go Beyond Taylor's Law, Journal of Integer Sequences 25 (2022), Article 22.9.3, mean/variance definitions, lines 119–124, equation at line 122, first equality of the equation at line 123, https://cs.uwaterloo.ca/journals/JIS/VOL25/Cohen/cohen13.tex.

Used by 1

Used byTaylor's law, asymptotic form

DefinitionTaylor's law, asymptotic form#✓fully proved

A sequence \(a : \mathbb{N} \to \mathbb{N}\), indexed from \(1\) (its value at \(0\) is ignored), satisfies Taylor's law asymptotically when it is admissible for Taylor's law and, writing \(m(a, n)\) and \(v(a, n)\) for its initial-segment mean and initial-segment sample variance, there are real numbers \(c > 0\) and \(b\) such that \(v(a, n) / m(a, n)^b \to c\) as \(n \to \infty\).

def SatisfiesTaylorsLawAsymptotically (a : ℕ → ℕ) : Prop :=
  IsTaylorAdmissibleSequence a ∧ ∃ c b : ℝ, 0 < c ∧
    Filter.Tendsto
      (fun n : ℕ => initialSegmentSampleVariance a n /
        Real.rpow (initialSegmentMean a n) b)
      Filter.atTop (nhds c)

Sources

• Joel E. Cohen, Variance Functions of Asymptotically Exponentially Increasing Integer Sequences Go Beyond Taylor's Law, Journal of Integer Sequences 25 (2022), Article 22.9.3, https://cs.uwaterloo.ca/journals/JIS/VOL25/Cohen/cohen13.tex: the collection 𝒜 of admissible sequences with the mean eq:mean and variance eq:varexpanded definitions (lines 113–125), and the asymptotic power-law definition eq:TLpower (lines 152–156).

Uses 3

Statement usesAdmissible sequences for Taylor's law · Initial-segment mean · Initial-segment sample variance

4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.