Fourier computation of weighted linkage disequilibrium

14 fully proved

Binning by grid-cell offset

DefinitionTotal of a per-SNP quantity over a grid cell#✓fully proved

The total U k = ∑_{x : c x = k} u x of a per-SNP quantity u over grid cell k.

def cellSum (u : S → ℝ) (k : ℕ) : ℝ := ∑ x with c x = k, u x

Used by 4

Used byPair count as autocorrelation of cell occupancy counts · ALDER's Fourier-transform weighted LD computation · ALDER's transform algorithm equals the brute-force weighted LD · Pair sum as cross-correlation of cell totals

DefinitionBrute-force pair sum at a cell offset#✓fully proved

The brute-force sum ∑_{x, y : c y = c x + j} u x v y over ordered SNP pairs whose grid cells differ by j.

def pairSum (u v : S → ℝ) (j : ℕ) : ℝ := ∑ x, ∑ y, if c y = c x + j then u x * v y else 0

Used by 3

Used byPair count as autocorrelation of cell occupancy counts · ALDER's transform algorithm equals the brute-force weighted LD · Pair sum as cross-correlation of cell totals

TheoremPair sum as cross-correlation of cell totals#✓fully proved

Grouping pairs by cell offset: if every SNP lies in a cell c x < K, the pair sum at offset j is the lag-j cross-correlation of the cell totals.

theorem pairSum_eq_sum_cellSum {K : ℕ} (hc : ∀ x, c x < K) (u v : S → ℝ) (j : ℕ) :
    pairSum c u v j = ∑ k ∈ Finset.range K, cellSum c u k * cellSum c v (k + j)

Uses 2 · Used by 2

Statement usesTotal of a per-SNP quantity over a grid cell · Brute-force pair sum at a cell offset

Used byPair count as autocorrelation of cell occupancy counts · ALDER's transform algorithm equals the brute-force weighted LD

Autocorrelation through the discrete Fourier transform

DefinitionZero padding of a sequence to \(\mathbb{Z}/N\mathbb{Z}\)#✓fully proved

Zero padding: the sequence U read on ZMod N through k ↦ U k.val. When U vanishes from K on and K ≤ N, this is U followed by N - K zeros.

def pad (N : ℕ) (U : ℕ → ℝ) : ZMod N → ℂ := fun k => (U k.val : ℂ)

Used by 2

Used byAutocorrelation via the discrete Fourier transform · Zero-padded circular autocorrelation equals linear autocorrelation

DefinitionAutocorrelation via the discrete Fourier transform#✓fully proved

The transform computation of the lag-j autocorrelation: the inverse discrete Fourier transform of the power spectrum |𝓕 Ũ|^2 of the zero-padded sequence, read at j.

noncomputable def autocorrDFT (N : ℕ) [NeZero N] (U : ℕ → ℝ) (j : ℕ) : ℂ :=
  𝓕⁻ (fun ξ => (Complex.normSq (𝓕 (pad N U) ξ) : ℂ)) (j : ZMod N)

Uses 1 · Used by 4

Statement usesZero padding of a sequence to \(\mathbb{Z}/N\mathbb{Z}\)

Used byPair count as autocorrelation of cell occupancy counts · Zero-padded circular autocorrelation equals linear autocorrelation · ALDER's Fourier-transform weighted LD computation · ALDER's transform algorithm equals the brute-force weighted LD

TheoremZero-padded circular autocorrelation equals linear autocorrelation#✓fully proved

Zero-padded circular autocorrelation equals the linear one: if U k = 0 for k ≥ K, 2 K ≤ N + 1 and j < K, then 𝓕⁻(|𝓕 Ũ|^2)(j) = ∑_{k < K} U k U (k + j).

theorem autocorrDFT_eq {N K : ℕ} [NeZero N] {U : ℕ → ℝ} (hU : ∀ k, K ≤ k → U k = 0)
    (hN : 2 * K ≤ N + 1) {j : ℕ} (hj : j < K) :
    autocorrDFT N U j = ((∑ k ∈ Finset.range K, U k * U (k + j) : ℝ) : ℂ)

Uses 3 · Used by 2

Statement usesAutocorrelation via the discrete Fourier transform

Proof usesZero padding of a sequence to \(\mathbb{Z}/N\mathbb{Z}\) · Convolution theorem for the discrete Fourier transform

Used byPair count as autocorrelation of cell occupancy counts · ALDER's transform algorithm equals the brute-force weighted LD

Weighted LD

DefinitionSample mean genotype at a SNP#✓fully proved

The sample mean genotype ḡ(x) = (1/m) ∑ i, g i x at SNP x over m individuals.

noncomputable def meanGeno (x : S) : ℝ := (∑ i, g i x) / m

Used by 3

Used byCentred weighted genotype · ALDER's transform algorithm equals the brute-force weighted LD · Unbiased sample covariance of genotypes

DefinitionUnbiased sample covariance of genotypes#✓fully proved

The unbiased sample covariance ẑ(x, y) = (1/(m - 1)) ∑ i, (g i x - ḡ x) (g i y - ḡ y) of the genotypes at SNPs x and y (Loh et al. 2013, Eq. 5; meaningful for m ≥ 2).

noncomputable def sampleCov (x y : S) : ℝ :=
  (∑ i, (g i x - meanGeno g x) * (g i y - meanGeno g y)) / ((m : ℝ) - 1)

Uses 1 · Used by 1

Statement usesSample mean genotype at a SNP

Used byBrute-force weighted linkage disequilibrium sum

DefinitionBrute-force weighted linkage disequilibrium sum#✓fully proved

The brute-force weighted-LD sum at cell offset j: ∑_{x, y : c y = c x + j} ẑ(x, y) w(x) w(y), costing a pass over all pairs.

noncomputable def bruteWeightedLD (j : ℕ) : ℝ :=
  ∑ x, ∑ y, if c y = c x + j then sampleCov g x y * w x * w y else 0

Uses 1 · Used by 1

Statement usesUnbiased sample covariance of genotypes

Used byALDER's transform algorithm equals the brute-force weighted LD

DefinitionCentred weighted genotype#✓fully proved

The centred weighted genotype (g i x - ḡ x) w x of individual i at SNP x.

noncomputable def centredWeighted (i : Fin m) (x : S) : ℝ := (g i x - meanGeno g x) * w x

Uses 1 · Used by 2

Statement usesSample mean genotype at a SNP

Used byALDER's Fourier-transform weighted LD computation · ALDER's transform algorithm equals the brute-force weighted LD

DefinitionALDER's Fourier-transform weighted LD computation#✓fully proved

ALDER's transform algorithm: for each individual, the zero-padded autocorrelation of the cell totals of its centred weighted genotypes, computed through 𝓕; summed over individuals and divided by m - 1.

noncomputable def dftWeightedLD (N : ℕ) [NeZero N] (j : ℕ) : ℂ :=
  (∑ i, autocorrDFT N (cellSum c (centredWeighted g w i)) j) / ((m : ℂ) - 1)

Uses 3 · Used by 1

Statement usesAutocorrelation via the discrete Fourier transform · Total of a per-SNP quantity over a grid cell · Centred weighted genotype

Used byALDER's transform algorithm equals the brute-force weighted LD

TheoremALDER's transform algorithm equals the brute-force weighted LD#✓fully proved

The transform algorithm computes the brute-force weighted-LD sum exactly, for every lag j < K, when all SNPs lie in cells c x < K and the transform length satisfies 2 K ≤ N + 1.

theorem dftWeightedLD_eq_bruteWeightedLD {N K : ℕ} [NeZero N] (hc : ∀ x, c x < K)
    (hN : 2 * K ≤ N + 1) {j : ℕ} (hj : j < K) :
    dftWeightedLD c g w N j = (bruteWeightedLD c g w j : ℂ)

Uses 9

Statement usesBrute-force weighted linkage disequilibrium sum · ALDER's Fourier-transform weighted LD computation

Proof usesAutocorrelation via the discrete Fourier transform · Zero-padded circular autocorrelation equals linear autocorrelation · Total of a per-SNP quantity over a grid cell · Centred weighted genotype · Sample mean genotype at a SNP · Brute-force pair sum at a cell offset · Pair sum as cross-correlation of cell totals

DefinitionNumber of SNP pairs at a cell offset#✓fully proved

The number of ordered SNP pairs at cell offset j, by which ALDER divides the weighted sum.

def pairCount (j : ℕ) : ℕ := ∑ x, ∑ y, if c y = c x + j then 1 else 0

Used by 1

Used byPair count as autocorrelation of cell occupancy counts

TheoremPair count as autocorrelation of cell occupancy counts#✓fully proved

The pair count is the zero-padded autocorrelation of the cell occupancy counts.

theorem autocorrDFT_cellCount {N K : ℕ} [NeZero N] (hc : ∀ x, c x < K)
    (hN : 2 * K ≤ N + 1) {j : ℕ} (hj : j < K) :
    autocorrDFT N (cellSum c fun _ => 1) j = (pairCount c j : ℂ)

Uses 6

Statement usesAutocorrelation via the discrete Fourier transform · Total of a per-SNP quantity over a grid cell · Number of SNP pairs at a cell offset

Proof usesZero-padded circular autocorrelation equals linear autocorrelation · Brute-force pair sum at a cell offset · Pair sum as cross-correlation of cell totals

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.