The sticky (equal-input) kernel on a finite state space

DefinitionEqual-input matrix#✓fully proved

The equal-input matrix 𝟙 πᵀ: every row equals π.

def equalInput (π : ι → ℝ) : Matrix ι ι ℝ :=
  Matrix.of fun _ j => π j

Used by 11

Used byContinuity of the sticky kernel in the persistence · The sticky kernel is the equal-input transition function · Entries of the equal-input matrix · Equal-input matrix is idempotent · Equal-input generator (F81 model) · Equal-input generator is a rate matrix · Sticky kernel · Composition · Sticky kernel at persistence one is the identity · Sticky kernel at persistence zero is the equal-input matrix · Long-distance limit

DefinitionSticky kernel#✓fully proved

The sticky kernel with persistence c: c • 1 + (1 - c) • 𝟙 πᵀ. Started from i, it stays at i with probability c and otherwise redraws the state from π.

noncomputable def stickyKernel [DecidableEq ι] (π : ι → ℝ) (c : ℝ) : Matrix ι ι ℝ :=
  c • (1 : Matrix ι ι ℝ) + (1 - c) • equalInput π

Uses 1 · Used by 17

Statement usesEqual-input matrix

Used byContinuity of the sticky kernel in the persistence · Two-state ancestry covariance · Covariance under the sticky kernel · The sticky kernel is the equal-input transition function · Entries of the sticky kernel · Semigroup law · Sticky kernel is row-stochastic · Composition · Nonnegativity of the sticky kernel · Sticky kernel at persistence one is the identity · Powers of the sticky kernel · Reversibility · Sticky kernel at persistence zero is the equal-input matrix · Rows of the sticky kernel sum to one · Long-distance limit · Short-distance limit · Stationary vector of the sticky kernel

DefinitionEqual-input generator (F81 model)#✓fully proved

The equal-input generator κ • (𝟙 πᵀ - 1) with rate κ (Felsenstein's F81 model on an arbitrary finite state space): jumps at rate κ to a state drawn from π.

noncomputable def equalInputRate [DecidableEq ι] (π : ι → ℝ) (κ : ℝ) : Matrix ι ι ℝ :=
  κ • (equalInput π - 1)

Uses 1 · Used by 2

Statement usesEqual-input matrix

Used byThe sticky kernel is the equal-input transition function · Equal-input generator is a rate matrix

TheoremEntries of the equal-input matrix#✓fully proved

Entrywise form of the equal-input matrix.

@[simp]
theorem equalInput_apply (π : ι → ℝ) (i j : ι) : equalInput π i j = π j

Uses 1

Statement usesEqual-input matrix

TheoremEqual-input matrix is idempotent#✓fully proved

With ∑ π = 1, 𝟙 πᵀ is idempotent.

theorem equalInput_mul_self [Fintype ι] (hπ : ∑ i, π i = 1) :
    equalInput π * equalInput π = equalInput π

Uses 1 · Used by 2

Statement usesEqual-input matrix

Used byThe sticky kernel is the equal-input transition function · Composition

TheoremEntries of the sticky kernel#✓fully proved

Entrywise form of the sticky kernel.

theorem stickyKernel_apply (π : ι → ℝ) (c : ℝ) (i j : ι) :
    stickyKernel π c i j = c * (if i = j then 1 else 0) + (1 - c) * π j

Uses 1 · Used by 4

Statement usesSticky kernel

Used byCovariance under the sticky kernel · Nonnegativity of the sticky kernel · Reversibility · Rows of the sticky kernel sum to one

TheoremSticky kernel at persistence one is the identity#✓fully proved

The sticky kernel at persistence 1 is the identity.

@[simp]
theorem stickyKernel_one (π : ι → ℝ) : stickyKernel π 1 = 1

Uses 2 · Used by 2

Statement usesSticky kernel

Proof usesEqual-input matrix

Used byPowers of the sticky kernel · Short-distance limit

TheoremSticky kernel at persistence zero is the equal-input matrix#✓fully proved

The sticky kernel at persistence 0 is 𝟙 πᵀ.

@[simp]
theorem stickyKernel_zero (π : ι → ℝ) : stickyKernel π 0 = equalInput π

Uses 2 · Used by 1

Statement usesEqual-input matrix · Sticky kernel

Used byLong-distance limit

TheoremNonnegativity of the sticky kernel#✓fully proved

For 0 ≤ c ≤ 1 and π ≥ 0 the entries of the sticky kernel are nonnegative.

theorem stickyKernel_nonneg (hπ : ∀ i, 0 ≤ π i) {c : ℝ} (hc0 : 0 ≤ c) (hc1 : c ≤ 1)
    (i j : ι) : 0 ≤ stickyKernel π c i j

Uses 2 · Used by 1

Statement usesSticky kernel

Proof usesEntries of the sticky kernel

Used bySticky kernel is row-stochastic

TheoremReversibility#✓fully proved

π i K i j = π j K j i (detailed balance), for all real c, π.

theorem stickyKernel_reversible (π : ι → ℝ) (c : ℝ) (i j : ι) :
    π i * stickyKernel π c i j = π j * stickyKernel π c j i

Uses 2 · Used by 1

Statement usesSticky kernel

Proof usesEntries of the sticky kernel

Used byStationary vector of the sticky kernel

TheoremContinuity of the sticky kernel in the persistence#✓fully proved

The sticky kernel depends continuously on the persistence.

theorem continuous_stickyKernel (π : ι → ℝ) : Continuous (stickyKernel π)

Uses 2 · Used by 2

Statement usesSticky kernel

Proof usesEqual-input matrix

Used byLong-distance limit · Short-distance limit

TheoremLong-distance limit#✓fully proved

For κ > 0, K (e^{-κ t}) → 𝟙 πᵀ as t → ∞.

theorem tendsto_stickyKernel_atTop (π : ι → ℝ) {κ : ℝ} (hκ : 0 < κ) :
    Tendsto (fun t => stickyKernel π (Real.exp (-(κ * t)))) atTop (𝓝 (equalInput π))

Uses 4

Statement usesEqual-input matrix · Sticky kernel

Proof usesContinuity of the sticky kernel in the persistence · Sticky kernel at persistence zero is the equal-input matrix

TheoremShort-distance limit#✓fully proved

K (e^{-κ t}) → 1 as t → 0, for every real κ.

theorem tendsto_stickyKernel_nhds_zero (π : ι → ℝ) (κ : ℝ) :
    Tendsto (fun t => stickyKernel π (Real.exp (-(κ * t)))) (𝓝 0) (𝓝 1)

Uses 3

Statement usesSticky kernel

Proof usesContinuity of the sticky kernel in the persistence · Sticky kernel at persistence one is the identity

TheoremRows of the sticky kernel sum to one#✓fully proved

With ∑ π = 1, the rows of the sticky kernel sum to 1 (for every real c).

theorem sum_stickyKernel (hπ : ∑ i, π i = 1) (c : ℝ) (i : ι) :
    ∑ j, stickyKernel π c i j = 1

Uses 2 · Used by 2

Statement usesSticky kernel

Proof usesEntries of the sticky kernel

Used bySticky kernel is row-stochastic · Stationary vector of the sticky kernel

TheoremSticky kernel is row-stochastic#✓fully proved

For 0 ≤ c ≤ 1, π ≥ 0 and ∑ π = 1 the sticky kernel is row-stochastic.

theorem stickyKernel_mem_rowStochastic (hπ0 : ∀ i, 0 ≤ π i) (hπ : ∑ i, π i = 1) {c : ℝ}
    (hc0 : 0 ≤ c) (hc1 : c ≤ 1) : stickyKernel π c ∈ rowStochastic ℝ ι

Uses 3

Statement usesSticky kernel

Proof usesNonnegativity of the sticky kernel · Rows of the sticky kernel sum to one

TheoremStationary vector of the sticky kernel#✓fully proved

With ∑ π = 1, π is a stationary vector of the sticky kernel: π K = π.

theorem vecMul_stickyKernel (hπ : ∑ i, π i = 1) (c : ℝ) : π ᵥ* stickyKernel π c = π

Uses 3

Statement usesSticky kernel

Proof usesReversibility · Rows of the sticky kernel sum to one

TheoremComposition#✓fully proved

With ∑ π = 1, K c * K c' = K (c c') for all real c, c'.

theorem stickyKernel_mul (hπ : ∑ i, π i = 1) (c c' : ℝ) :
    stickyKernel π c * stickyKernel π c' = stickyKernel π (c * c')

Uses 3 · Used by 2

Statement usesSticky kernel

Proof usesEqual-input matrix · Equal-input matrix is idempotent

Used bySemigroup law · Powers of the sticky kernel

TheoremPowers of the sticky kernel#✓fully proved

With ∑ π = 1, K c ^ n = K (c ^ n): n steps of the sticky kernel are one step with persistence c ^ n.

theorem stickyKernel_pow (hπ : ∑ i, π i = 1) (c : ℝ) (n : ℕ) :
    stickyKernel π c ^ n = stickyKernel π (c ^ n)

Uses 3

Statement usesSticky kernel

Proof usesComposition · Sticky kernel at persistence one is the identity

TheoremEqual-input generator is a rate matrix#✓fully proved

For κ ≥ 0, π ≥ 0 and ∑ π = 1, the equal-input generator is a rate matrix.

theorem isRateMatrix_equalInputRate (hπ0 : ∀ i, 0 ≤ π i) (hπ : ∑ i, π i = 1) {κ : ℝ}
    (hκ : 0 ≤ κ) : IsRateMatrix (equalInputRate π κ)

Uses 3

Statement usesRate matrix · Equal-input generator (F81 model)

Proof usesEqual-input matrix

TheoremThe sticky kernel is the equal-input transition function#✓fully proved

With ∑ π = 1, exp (t • κ (𝟙 πᵀ - 1)) = K (e^{-κ t}) for all real κ and t.

theorem ctmcTransition_equalInputRate (hπ : ∑ i, π i = 1) (κ t : ℝ) :
    ctmcTransition (equalInputRate π κ) t = stickyKernel π (Real.exp (-(κ * t)))

Uses 5

Statement usesTransition semigroup of a continuous-time Markov chain · Equal-input generator (F81 model) · Sticky kernel

Proof usesEqual-input matrix · Equal-input matrix is idempotent

TheoremSemigroup law#✓fully proved

Semigroup law of the sticky kernel in time: K (e^{-κ s}) * K (e^{-κ t}) = K (e^{-κ (s + t)}) (with ∑ π = 1).

theorem stickyKernel_exp_add (hπ : ∑ i, π i = 1) (κ s t : ℝ) :
    stickyKernel π (Real.exp (-(κ * s))) * stickyKernel π (Real.exp (-(κ * t))) =
      stickyKernel π (Real.exp (-(κ * (s + t))))

Uses 2

Statement usesSticky kernel

Proof usesComposition

TheoremCovariance under the sticky kernel#✓fully proved

If (X, Y) has joint law P(X = i, Y = j) = π i K i j (stationary start, one step of the kernel), then Cov(f X, g Y) = c Cov_π(f, g). The algebraic identity holds for all real π, f, g, c; it is a covariance of a probability law when π is a probability vector and 0 ≤ c ≤ 1.

theorem covariance_stickyKernel (π : ι → ℝ) (c : ℝ) (f g : ι → ℝ) :
    ∑ i, ∑ j, π i * stickyKernel π c i j * (f i * g j) -
        (∑ i, π i * f i) * (∑ j, π j * g j) =
      c * (∑ i, π i * (f i * g i) - (∑ i, π i * f i) * (∑ j, π j * g j))

Uses 2 · Used by 1

Statement usesSticky kernel

Proof usesEntries of the sticky kernel

Used byTwo-state ancestry covariance

TheoremTwo-state ancestry covariance#✓fully proved

Two-state ancestry covariance (the local-ancestry chain of a two-way pulse admixture). With ancestry proportions π = (α, 1 - α) and persistence c = (1 - r) ^ n (no recombination between the two sites along the n meioses since admixture, recombination fraction r per meiosis), the indicators I_x = [X = 0], I_y = [Y = 0] of ancestry 0 at the two sites have covariance α (1 - α) (1 - r) ^ n. The kernel form of the ancestry pair is the modeling assumption here; this statement does not derive it from a genealogy.

theorem covariance_indicator_stickyKernel_two (α r : ℝ) (n : ℕ) :
    let π : Fin 2 → ℝ := ![α, 1 - α]
    let I : Fin 2 → ℝ := ![1, 0]
    ∑ i, ∑ j, π i * stickyKernel π ((1 - r) ^ n) i j * (I i * I j) -
        (∑ i, π i * I i) * (∑ j, π j * I j) = α * (1 - α) * (1 - r) ^ n

Uses 2

Statement usesSticky kernel

Proof usesCovariance under the sticky kernel

23 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.