Extended haplotype homozygosity

15 fully proved

Sample

DefinitionHaplotype window around the core#✓fully proved

The window of radius d of haplotype i: its alleles at the d sites closest to the core, in the direction indexed by ℕ.

def window (h : ι → ℕ → α) (d : ℕ) (i : ι) : Fin d → α := fun k => h i k

Used by 6

Used byConcordant haplotype pairs at a given radius · Concordant haplotype pairs sharing a core allele · EHH is nonincreasing in the radius · EHH as homozygosity of window-type counts · EHH at radius zero equals one · Equality of haplotype windows

TheoremEquality of haplotype windows#✓fully proved

Two haplotypes have the same window of radius d exactly when they agree at every site k < d.

theorem window_eq_iff (h : ι → ℕ → α) (d : ℕ) (i j : ι) :
    window h d i = window h d j ↔ ∀ k < d, h i k = h j k

Uses 1 · Used by 1

Statement usesHaplotype window around the core

Used byEHH is nonincreasing in the radius

DefinitionConcordant haplotype pairs at a given radius#✓fully proved

The number of ordered pairs of distinct haplotypes of C whose windows of radius d agree.

def concordantPairs (h : ι → ℕ → α) (C : Finset ι) (d : ℕ) : ℕ :=
  ((C ×ˢ C).filter fun p => p.1 ≠ p.2 ∧ window h d p.1 = window h d p.2).card

Uses 1 · Used by 5

Statement usesHaplotype window around the core

Used byExtended haplotype homozygosity (EHH) · EHH is nonincreasing in the radius · EHH as homozygosity of window-type counts · EHH is zero for a set of at most one haplotype · EHH at radius zero equals one

DefinitionExtended haplotype homozygosity (EHH)#✓fully proved

Extended haplotype homozygosity at radius d of the haplotype set C: the probability that two distinct haplotypes drawn from C without replacement agree at all d sites nearest the core (Sabeti et al. 2002). For #C ≤ 1 the denominator vanishes and the junk value 0 is returned; every statement below that needs the probabilistic reading assumes 2 ≤ #C.

noncomputable def ehh (h : ι → ℕ → α) (C : Finset ι) (d : ℕ) : ℝ :=
  (concordantPairs h C d : ℝ) / ((C.card : ℝ) * ((C.card : ℝ) - 1))

Uses 1 · Used by 4

Statement usesConcordant haplotype pairs at a given radius

Used byEHH is nonincreasing in the radius · EHH as homozygosity of window-type counts · EHH is zero for a set of at most one haplotype · EHH at radius zero equals one

TheoremEHH is zero for a set of at most one haplotype#✓fully proved

Outside the domain 2 ≤ #C the definition returns the junk value 0.

theorem ehh_eq_zero_of_card_le_one (h : ι → ℕ → α) {C : Finset ι} (hC : C.card ≤ 1) (d : ℕ) :
    ehh h C d = 0

Uses 2 · Used by 1

Statement usesExtended haplotype homozygosity (EHH)

Proof usesConcordant haplotype pairs at a given radius

Used byEHH is nonincreasing in the radius

TheoremEHH at radius zero equals one#✓fully proved

At radius 0 every pair of haplotypes agrees, so EHH(0) = 1.

theorem ehh_zero_window (h : ι → ℕ → α) {C : Finset ι} (hC : 2 ≤ C.card) :
    ehh h C 0 = 1

Uses 3

Statement usesExtended haplotype homozygosity (EHH)

Proof usesConcordant haplotype pairs at a given radius · Haplotype window around the core

TheoremEHH is nonincreasing in the radius#✓fully proved

EHH is nonincreasing in the radius: widening the window can only break ties.

theorem ehh_antitone (h : ι → ℕ → α) (C : Finset ι) {d d' : ℕ} (hd : d ≤ d') :
    ehh h C d' ≤ ehh h C d

Uses 5

Statement usesExtended haplotype homozygosity (EHH)

Proof usesConcordant haplotype pairs at a given radius · EHH is zero for a set of at most one haplotype · Haplotype window around the core · Equality of haplotype windows

TheoremEHH as homozygosity of window-type counts#✓fully proved

EHH as the sampling-without-replacement homozygosity of the partition of C into window types: EHH(d) = ∑_t c_t (c_t - 1) / (#C (#C - 1)), where c_t is the number of haplotypes of C with window t. This is the form in which EHH is usually defined.

theorem ehh_eq_sum_counts (h : ι → ℕ → α) (C : Finset ι) (d : ℕ) :
    ehh h C d = (∑ t ∈ C.image (window h d),
        ((C.filter fun i => window h d i = t).card : ℝ) *
          (((C.filter fun i => window h d i = t).card : ℝ) - 1)) /
      ((C.card : ℝ) * ((C.card : ℝ) - 1))

Uses 3

Statement usesExtended haplotype homozygosity (EHH) · Haplotype window around the core

Proof usesConcordant haplotype pairs at a given radius

DefinitionConcordant haplotype pairs sharing a core allele#✓fully proved

The number of ordered pairs of distinct haplotypes of C whose core alleles (under core) agree and whose windows of radius d agree. The extended haplotype includes the core, so pairs carrying different core alleles are never concordant, even when their outward windows match.

def concordantPairsCore {β : Type*} [DecidableEq β] (core : ι → β) (h : ι → ℕ → α)
    (C : Finset ι) (d : ℕ) : ℕ :=
  ((C ×ˢ C).filter fun p =>
    p.1 ≠ p.2 ∧ core p.1 = core p.2 ∧ window h d p.1 = window h d p.2).card

Uses 1 · Used by 1

Statement usesHaplotype window around the core

Used byExtended haplotype homozygosity with core-allele labels

DefinitionExtended haplotype homozygosity with core-allele labels#✓fully proved

Extended haplotype homozygosity with core-allele labels: the probability that two distinct haplotypes drawn from C without replacement share both their core allele and their window of radius d. For a set C of carriers of a single core allele this is the same count as ehh; for a pooled set D carrying several core alleles it excludes the cross-core pairs that plain ehh would wrongly count as concordant.

noncomputable def ehhCore {β : Type*} [DecidableEq β] (core : ι → β) (h : ι → ℕ → α)
    (C : Finset ι) (d : ℕ) : ℝ :=
  (concordantPairsCore core h C d : ℝ) / ((C.card : ℝ) * ((C.card : ℝ) - 1))

Uses 1 · Used by 2

Statement usesConcordant haplotype pairs sharing a core allele

Used byCriterion for relative EHH to exceed one · Relative extended haplotype homozygosity (REHH)

DefinitionRelative extended haplotype homozygosity (REHH)#✓fully proved

Relative extended haplotype homozygosity: the core-labelled EHH of the core-allele carriers C divided by the core-labelled EHH of the pooled set D of haplotypes carrying the other core alleles. The denominator counts only pairs sharing a core allele, so cross-core pairs never inflate it. This is the statistic of the long-range haplotype test (Sabeti et al. 2002). It is a junk value 0 when the denominator vanishes; one_lt_rehh_iff assumes a positive denominator.

noncomputable def rehh {β : Type*} [DecidableEq β] (core : ι → β) (h : ι → ℕ → α)
    (C D : Finset ι) (d : ℕ) : ℝ :=
  ehhCore core h C d / ehhCore core h D d

Uses 1 · Used by 1

Statement usesExtended haplotype homozygosity with core-allele labels

Used byCriterion for relative EHH to exceed one

TheoremCriterion for relative EHH to exceed one#✓fully proved

With a positive reference EHH, the relative EHH exceeds 1 exactly when the core allele's haplotypes are the more homozygous ones.

theorem one_lt_rehh_iff {β : Type*} [DecidableEq β] (core : ι → β) (h : ι → ℕ → α)
    (C D : Finset ι) {d : ℕ} (hD : 0 < ehhCore core h D d) :
    1 < rehh core h C D d ↔ ehhCore core h D d < ehhCore core h C d

Uses 2

Statement usesExtended haplotype homozygosity with core-allele labels · Relative extended haplotype homozygosity (REHH)

Neutral

DefinitionProbability of no recombination on a pair's genealogy#✓fully proved

The probability that no recombination falls on the genealogy of a pair of lineages within genetic distance d of the core, given that the pair coalesces at time t (time in units of 2N generations, ρ = 4Nr the scaled recombination rate per site): the two lineages carry recombination events at total rate ρ * d until they coalesce.

In a mutation-free model this is a lower bound for the probability that the two haplotypes are identical over the window — no recombination then implies identical windows, while a recombined lineage may still carry the same alleles — so it is a lower bound for the expected EHH, not its value. Without the mutation-free assumption the bound is not established: mutations on either descendant branch can make the haplotypes differ even with no recombination.

noncomputable def pairNoRecomb (ρ d t : ℝ) : ℝ := exp (-(ρ * d) * t)

Used by 2

Used byMean no-recombination probability under the neutral coalescent · No-recombination probability decays with distance

TheoremNo-recombination probability decays with distance#✓fully proved

The no-recombination probability decays in the distance from the core.

theorem pairNoRecomb_antitone {ρ t : ℝ} (hρ : 0 ≤ ρ) (ht : 0 ≤ t) {d d' : ℝ} (hd : d ≤ d') :
    pairNoRecomb ρ d' t ≤ pairNoRecomb ρ d t

Uses 1

Statement usesProbability of no recombination on a pair's genealogy

TheoremMean no-recombination probability under the neutral coalescent#✓fully proved

Averaging over the pair coalescence time T₂, which is exponential of rate 1 in units of 2N generations under the neutral coalescent, the probability that no recombination falls on the pair's genealogy within distance d is 1 / (1 + ρ d). In a mutation-free model, since a recombined lineage can still carry an identical haplotype, this is a lower bound for E[EHH(d)]; without that assumption the bound is not established.

theorem integral_pairNoRecomb {ρ d : ℝ} (hρ : 0 ≤ ρ) (hd : 0 ≤ d) :
    ∫ t, pairNoRecomb ρ d t ∂(expMeasure 1) = (1 + ρ * d)⁻¹

Uses 2

Statement usesProbability of no recombination on a pair's genealogy

Proof usesMoment generating function of the gamma distribution

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.