Fitting admixture graphs by least squares

DefinitionGeneralized least-squares qpGraph score S1#✓fully proved

The qpGraph score S1(g) = -½ (g - f)ᵀ Q⁻¹ (g - f) (Patterson et al. 2012, eq. 6) of predicted statistics g against estimated statistics f with error covariance Q.

noncomputable def scoreS1 [DecidableEq ι] (Q : Matrix ι ι ℝ) (f g : ι → ℝ) : ℝ :=
  -(1 / 2) * ((g - f) ⬝ᵥ (Q⁻¹ *ᵥ (g - f)))

Used by 4

Used byUniqueness of the generalized least-squares maximizer · Basis independence of the qpGraph score S1 · Solutions of the normal equations maximize the score S1 · Score S2 as score S1 with a diagonal covariance

DefinitionLeast-squares qpGraph score S2#✓fully proved

The least-squares qpGraph score S2(g) = -∑ᵢ (gᵢ - fᵢ)² / (Qᵢᵢ + λ) (Patterson et al. 2012, eq. 7). A term with Qᵢᵢ + λ = 0 is 0 by the convention x / 0 = 0.

noncomputable def scoreS2 (Q : Matrix ι ι ℝ) (lam : ℝ) (f g : ι → ℝ) : ℝ :=
  -∑ i, (g i - f i) ^ 2 / (Q i i + lam)

Used by 2

Used byThe qpGraph score S2 depends on the basis · Score S2 as score S1 with a diagonal covariance

TheoremBasis independence of the qpGraph score S1#✓fully proved

S1 is basis independent: under an invertible change of basis A of the statistics, with the covariance transformed to A Q Aᵀ, the score is unchanged. (The identity holds for every Q; for singular Q both sides are 0 by Mathlib's convention Q⁻¹ = 0.)

theorem scoreS1_basis_change [DecidableEq ι] (A : Matrix ι ι ℝ) (hA : IsUnit A.det)
    (Q : Matrix ι ι ℝ)
    (f g : ι → ℝ) : scoreS1 (A * Q * Aᵀ) (A *ᵥ f) (A *ᵥ g) = scoreS1 Q f g

Uses 1

Statement usesGeneralized least-squares qpGraph score S1

TheoremThe qpGraph score S2 depends on the basis#✓fully proved

S2 is not basis independent (Patterson et al. 2012, after eq. 7): there are a positive definite covariance Q, an invertible change of basis A and statistics f, g such that, for every λ, the score changes.

theorem exists_scoreS2_basis_change_ne :
    ∃ (Q A : Matrix (Fin 2) (Fin 2) ℝ) (f g : Fin 2 → ℝ), Q.PosDef ∧ IsUnit A.det ∧
      ∀ lam : ℝ, scoreS2 (A * Q * Aᵀ) lam (A *ᵥ f) (A *ᵥ g) ≠ scoreS2 Q lam f g

Uses 1

Statement usesLeast-squares qpGraph score S2

TheoremScore S2 as score S1 with a diagonal covariance#✓fully proved

S2 is twice S1 with the covariance replaced by the diagonal matrix of the Qᵢᵢ + λ, when these are nonzero.

theorem scoreS2_eq_scoreS1_diagonal [DecidableEq ι] (Q : Matrix ι ι ℝ) (lam : ℝ)
    (h : ∀ i, Q i i + lam ≠ 0)
    (f g : ι → ℝ) :
    scoreS2 Q lam f g = 2 * scoreS1 (diagonal fun i => Q i i + lam) f g

Uses 2

Statement usesGeneralized least-squares qpGraph score S1 · Least-squares qpGraph score S2

DefinitionqpGraph design matrix of basis f4 statistics#✓fully proved

The qpGraph design matrix of basis statistics f4 (A i) (B i) (C i) (D i) for lineage weights w: entry (i, e) is (w Aᵢ e - w Bᵢ e) * (w Cᵢ e - w Dᵢ e).

def designMatrix {ι E P : Type*} (w : P → E → ℝ) (A B C D : ι → P) : Matrix ι E ℝ :=
  fun i e => (w (A i) e - w (B i) e) * (w (C i) e - w (D i) e)

Used by 1

Used byPredicted f4 statistics are linear in the edge lengths

TheoremPredicted f4 statistics are linear in the edge lengths#✓fully proved

In the drift model, with the admixture weights fixed, the predicted statistics are linear in the edge lengths: g = B ℓ for the design matrix B.

theorem f4_eq_designMatrix_mulVec {ι E Ω P : Type*} [Fintype E] {m : MeasurableSpace Ω}
    {μ : Measure Ω}
    (M : DriftModel μ E P) (A B C D : ι → P) :
    (fun i => f4 μ M.freq (A i) (B i) (C i) (D i)) = designMatrix M.weight A B C D *ᵥ M.len

Uses 5

Statement usesAdmixture-graph drift model · Allele frequency of a population in the drift model · f4 statistic · qpGraph design matrix of basis f4 statistics

Proof usesf4 in the drift model

TheoremSolutions of the normal equations maximize the score S1#✓fully proved

GLS maximizes S1: for positive definite Q, a solution ℓ̂ of the normal equations Bᵀ Q⁻¹ B ℓ̂ = Bᵀ Q⁻¹ f maximizes ℓ ↦ S1(B ℓ) over all ℓ.

theorem scoreS1_le_of_normal_eq [DecidableEq ι] [Fintype E] {Q : Matrix ι ι ℝ} (hQ : Q.PosDef)
    (B : Matrix ι E ℝ)
    (f : ι → ℝ) {lhat : E → ℝ} (hnorm : (Bᵀ * Q⁻¹ * B) *ᵥ lhat = (Bᵀ * Q⁻¹) *ᵥ f)
    (l : E → ℝ) : scoreS1 Q f (B *ᵥ l) ≤ scoreS1 Q f (B *ᵥ lhat)

Uses 1

Statement usesGeneralized least-squares qpGraph score S1

TheoremUniqueness of the generalized least-squares maximizer#✓fully proved

Uniqueness of the GLS maximizer: for positive definite Q and a design matrix of full column rank (B.mulVec injective), a vector ℓ with the same score as a solution ℓ̂ of the normal equations equals ℓ̂.

theorem eq_of_scoreS1_eq [DecidableEq ι] [Fintype E] {Q : Matrix ι ι ℝ} (hQ : Q.PosDef)
    {B : Matrix ι E ℝ}
    (hB : Function.Injective B.mulVec) (f : ι → ℝ) {lhat : E → ℝ}
    (hnorm : (Bᵀ * Q⁻¹ * B) *ᵥ lhat = (Bᵀ * Q⁻¹) *ᵥ f) {l : E → ℝ}
    (h : scoreS1 Q f (B *ᵥ l) = scoreS1 Q f (B *ᵥ lhat)) : l = lhat

Uses 1

Statement usesGeneralized least-squares qpGraph score S1

TheoremInvertibility of the generalized least-squares Gram matrix#✓fully proved

For positive definite Q and a design matrix of full column rank, the GLS Gram matrix Bᵀ Q⁻¹ B is invertible.

theorem isUnit_det_gram [DecidableEq ι] [Fintype E] [DecidableEq E] {Q : Matrix ι ι ℝ}
    (hQ : Q.PosDef) {B : Matrix ι E ℝ}
    (hB : Function.Injective B.mulVec) : IsUnit (Bᵀ * Q⁻¹ * B).det

TheoremClosed-form generalized least-squares estimate of edge lengths#✓fully proved

The closed-form GLS estimate ℓ̂ = (Bᵀ Q⁻¹ B)⁻¹ Bᵀ Q⁻¹ f solves the normal equations when the Gram matrix is invertible.

theorem normal_eq_gls [DecidableEq ι] [Fintype E] [DecidableEq E] {Q : Matrix ι ι ℝ}
    {B : Matrix ι E ℝ} (h : IsUnit (Bᵀ * Q⁻¹ * B).det)
    (f : ι → ℝ) :
    (Bᵀ * Q⁻¹ * B) *ᵥ ((Bᵀ * Q⁻¹ * B)⁻¹ *ᵥ ((Bᵀ * Q⁻¹) *ᵥ f)) = (Bᵀ * Q⁻¹) *ᵥ f

11 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.