Centred population covariance and f-statistics

14 fully proved

Covariance

DefinitionMean frequency across populations#✓fully proved

The mean frequency p̄ ω = (1 / n) ∑ X, p X ω across the n populations.

noncomputable def popMean (p : P → Ω → ℝ) (ω : Ω) : ℝ := (∑ X, p X ω) / Fintype.card P

Used by 3

Used byCentred leaf covariance · Centred leaf covariance as the double centring of f2 · f2 from the centred leaf covariance

DefinitionCentred leaf covariance#✓fully proved

The centred leaf covariance K X Y = 𝔼[(p X - p̄) * (p Y - p̄)]: the second moments of the frequencies centred across populations (not over Ω).

noncomputable def centredCov (μ : Measure Ω) (p : P → Ω → ℝ) (X Y : P) : ℝ :=
  ∫ ω, (p X ω - popMean p ω) * (p Y ω - popMean p ω) ∂μ

Uses 1 · Used by 3

Statement usesMean frequency across populations

Used byCentred leaf covariance as the double centring of f2 · f2 from the centred leaf covariance · f-statistics determine exactly the centred leaf covariance

Theoremf2 from the centred leaf covariance#✓fully proved

f2 from the centred leaf covariance: f2 X Y = K X X + K Y Y - 2 K X Y.

theorem f2_eq_centredCov (hp : ∀ X, MemLp (p X) 2 μ) (X Y : P) :
    f2 μ p X Y = centredCov μ p X X + centredCov μ p Y Y - 2 * centredCov μ p X Y

Uses 3 · Used by 2

Statement usesf2 statistic · Centred leaf covariance

Proof usesMean frequency across populations

Used byCentred leaf covariance as the double centring of f2 · f-statistics determine exactly the centred leaf covariance

TheoremCentred leaf covariance as the double centring of f2#✓fully proved

The centred leaf covariance from f2: K is half the double centring of the f2 matrix, K X Y = (f̄2 X· + f̄2 ·Y - f2 X Y - f̄2 ··) / 2.

theorem centredCov_eq_doubleCenter_f2 (hp : ∀ X, MemLp (p X) 2 μ) (X Y : P) :
    centredCov μ p X Y = doubleCenter (f2 μ p) X Y / 2

Uses 5 · Used by 1

Statement usesDouble centring of a square matrix · f2 statistic · Centred leaf covariance

Proof usesf2 from the centred leaf covariance · Mean frequency across populations

Used byf-statistics determine exactly the centred leaf covariance

Theoremf-statistics determine exactly the centred leaf covariance#✓fully proved

f-statistics determine exactly the centred leaf covariance. f-statistics see a model only through its centred leaf covariance: two square-integrable frequency models have the same f2 at every pair (hence the same f3 and f4, by f3_eq_f2 and f4_eq_f2) if and only if they have the same centred leaf covariance.

theorem f2_eq_iff_centredCov_eq {Ω' : Type*} {m' : MeasurableSpace Ω'} {μ' : Measure Ω'}
    {p' : P → Ω' → ℝ} (hp : ∀ X, MemLp (p X) 2 μ) (hp' : ∀ X, MemLp (p' X) 2 μ') :
    (∀ X Y, f2 μ p X Y = f2 μ' p' X Y) ↔ ∀ X Y, centredCov μ p X Y = centredCov μ' p' X Y

Uses 5

Statement usesf2 statistic · Centred leaf covariance

Proof usesDouble centring of a square matrix · Centred leaf covariance as the double centring of f2 · f2 from the centred leaf covariance

Pair

DefinitionLineage weights of the three-population star tree#✓fully proved

Lineage weights of the star tree on three populations 0 = A, 1 = B, 2 = C: edge e is the leaf edge of population e.

def starWeight : Fin 3 → Fin 3 → ℝ := fun X e => if X = e then 1 else 0

Used by 6

Used byLineage weights of the three-population admixture model · Admixed population's weights in the admixture model · Star tree and admixture model have equal f2 · Star tree and admixture model have equal f4 · Star-tree model has binary loadings · Admixture model lacks binary loadings

DefinitionLineage weights of the three-population admixture model#✓fully proved

Lineage weights of the admixture model: A and B sit on edges 0 and 1, and C is an α : 1 - α mixture of A and B followed by drift on its private edge 2.

def admixWeight (α : ℝ) : Fin 3 → Fin 3 → ℝ :=
  fun X e => if X = 2 then ![α, 1 - α, 1] e else starWeight X e

Uses 1 · Used by 4

Statement usesLineage weights of the three-population star tree

Used byAdmixed population's weights in the admixture model · Star tree and admixture model have equal f2 · Star tree and admixture model have equal f4 · Admixture model lacks binary loadings

DefinitionEdge lengths of the star tree matching an admixture model#✓fully proved

Edge lengths of the star tree matching the admixture model with edge lengths a, b, c: (1 - α)(a + b), α (a + b) and c - α (1 - α)(a + b).

def starLen (α a b c : ℝ) : Fin 3 → ℝ :=
  ![(1 - α) * (a + b), α * (a + b), c - α * (1 - α) * (a + b)]

Used by 3

Used byStar tree and admixture model have equal f2 · Star tree and admixture model have equal f4 · Nonnegativity of the matching star-tree edge lengths

TheoremAdmixed population's weights in the admixture model#✓fully proved

In the admixture model, C is the α : 1 - α mixture of A and B plus its private edge.

theorem admixWeight_two (α : ℝ) :
    admixWeight α 2 = α • admixWeight α 0 + (1 - α) • admixWeight α 1 + Pi.single 2 1

Uses 2

Statement usesLineage weights of the three-population admixture model

Proof usesLineage weights of the three-population star tree

TheoremStar-tree model has binary loadings#✓fully proved

The star-tree model has binary loadings.

theorem hasBinaryLoadings_star {M : DriftModel μ (Fin 3) (Fin 3)} (hw : M.weight = starWeight) :
    M.HasBinaryLoadings

Uses 3

Statement usesAdmixture-graph drift model · Binary loadings of a drift model · Lineage weights of the three-population star tree

TheoremAdmixture model lacks binary loadings#✓fully proved

For α ∉ {0, 1} the admixture model does not have binary loadings.

theorem not_hasBinaryLoadings_admix {α : ℝ} (h0 : α ≠ 0) (h1 : α ≠ 1)
    {M : DriftModel μ (Fin 3) (Fin 3)} (hw : M.weight = admixWeight α) :
    ¬ M.HasBinaryLoadings

Uses 4

Statement usesAdmixture-graph drift model · Binary loadings of a drift model · Lineage weights of the three-population admixture model

Proof usesLineage weights of the three-population star tree

TheoremStar tree and admixture model have equal f2#✓fully proved

The star tree and the admixture model have the same f2 at every pair of populations.

theorem f2_star_eq_f2_admix {α a b c : ℝ} {M : DriftModel μ (Fin 3) (Fin 3)}
    {M' : DriftModel μ' (Fin 3) (Fin 3)} (hw : M.weight = starWeight)
    (hl : M.len = starLen α a b c) (hw' : M'.weight = admixWeight α) (hl' : M'.len = ![a, b, c])
    (X Y : Fin 3) : f2 μ M.freq X Y = f2 μ' M'.freq X Y

Uses 7 · Used by 1

Statement usesAdmixture-graph drift model · Allele frequency of a population in the drift model · f2 statistic · Lineage weights of the three-population admixture model · Edge lengths of the star tree matching an admixture model · Lineage weights of the three-population star tree

Proof usesf2 in the drift model

Used byStar tree and admixture model have equal f4

TheoremStar tree and admixture model have equal f4#✓fully proved

The star tree and the admixture model have the same f4 (hence the same f3) at every quadruple of populations.

theorem f4_star_eq_f4_admix {α a b c : ℝ} {M : DriftModel μ (Fin 3) (Fin 3)}
    {M' : DriftModel μ' (Fin 3) (Fin 3)} (hw : M.weight = starWeight)
    (hl : M.len = starLen α a b c) (hw' : M'.weight = admixWeight α) (hl' : M'.len = ![a, b, c])
    (A B C D : Fin 3) : f4 μ M.freq A B C D = f4 μ' M'.freq A B C D

Uses 10

Statement usesAdmixture-graph drift model · Allele frequency of a population in the drift model · f4 statistic · Lineage weights of the three-population admixture model · Edge lengths of the star tree matching an admixture model · Lineage weights of the three-population star tree

Proof usesPopulation frequencies are square integrable · f2 statistic · f4 in terms of f2 · Star tree and admixture model have equal f2

TheoremNonnegativity of the matching star-tree edge lengths#✓fully proved

The matching star tree has nonnegative edge lengths when 0 ≤ α ≤ 1, a, b ≥ 0, and the private drift of C is at least α (1 - α)(a + b), i.e. when f3 C A B ≥ 0 in the admixture model.

theorem starLen_nonneg {α a b c : ℝ} (hα0 : 0 ≤ α) (hα1 : α ≤ 1) (ha : 0 ≤ a) (hb : 0 ≤ b)
    (hc : α * (1 - α) * (a + b) ≤ c) (e : Fin 3) : 0 ≤ starLen α a b c e

Uses 1

Statement usesEdge lengths of the star tree matching an admixture model

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.